Pure type systems with more liberal rules

DOI10.2307/2694962zbMath0997.03014OpenAlexW2166708555MaRDI QIDQ4328821

Wil Dekkers, Martin W. Bunder

Publication date: 13 November 2002

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2694962

zbMATH Keywords

pure type systemsweakening ruleconversion rulelambda-cubeabstraction rulefoundation for proof assistantsstart rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Variants of the basic calculus of constructions ⋮ Bridging Curry and Church's typing style ⋮ Equivalences between pure type systems and systems of illative combinatory logic

Uses Software

• Automath

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• Scott's models and illative combinatory logic
• Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
• Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic
• Systems of illative combinatory logic complete for first-order propositional and predicate calculus
• On the proof theory of Coquand's calculus of constructions

This page was built for publication: Pure type systems with more liberal rules