Variants of the basic calculus of constructions

DOI10.1016/j.jal.2004.02.004zbMath1068.03012OpenAlexW1971671369MaRDI QIDQ1885480

Martin W. Bunder, Jonathan P. Seldin

Publication date: 28 October 2004

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

Full work available at URL: https://doi.org/10.1016/j.jal.2004.02.004

zbMATH Keywords

calculus of constructionstyped \(\lambda\)-calculuspure typed systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• Type inference for pure type systems
• A Gentzen-style sequent calculus of constructions with expansion rules
• Untersuchungen über das logische Schliessen. I
• Equivalences between pure type systems and systems of illative combinatory logic
• Extensional Set Equality in the Calculus of Constructions
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Progress report on generalized functionality
• Some Inconsistencies in Illative Combinatory Logic
• A sequent calculus for type assignment
• Pure type systems with more liberal rules
• Termination of rewriting in the Calculus of Constructions
• On lists and other abstract data types in the calculus of constructions
• Modularity of termination and confluence in combinations of rewrite systems with λω
• Domain-free pure type systems
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• On the proof theory of Coquand's calculus of constructions