Variants of the basic calculus of constructions

DOI10.1016/J.JAL.2004.02.004MaRDI QIDQ1885480zbMATH OpenOpenAlexFDO

Authors 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

typed \(\lambda\)-calculuscalculus of constructionspure typed systems

Mathematics Subject Classification ID

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

Recommendations

• On the proof theory of Coquand's calculus of constructions
• The calculus of constructions
• scientific article; zbMATH DE number 4014064
• Type checking with universes
• Coquand's calculus of constructions: A mathematical foundation for a proof development system

Cites work

• scientific article; zbMATH DE number 4019061 (Why is no real title available?)
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 512772 (Why is no real title available?)
• scientific article; zbMATH DE number 2043543 (Why is no real title available?)
• scientific article; zbMATH DE number 1377703 (Why is no real title available?)
• scientific article; zbMATH DE number 3261581 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 3062910 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• A Gentzen-style sequent calculus of constructions with expansion rules
• A sequent calculus for type assignment
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• Domain-free pure type systems
• Equivalences between pure type systems and systems of illative combinatory logic
• Extensional set equality in the calculus of constructions
• Modularity of termination and confluence in combinations of rewrite systems with \(\lambda_\omega\)
• On lists and other abstract data types in the calculus of constructions
• On the proof theory of Coquand's calculus of constructions
• Progress report on generalized functionality
• Pure type systems with more liberal rules
• Some Inconsistencies in Illative Combinatory Logic
• Termination of rewriting in the Calculus of Constructions
• The calculus of constructions
• Type inference for pure type systems
• Untersuchungen über das logische Schliessen. I

Cited in

(2)

• Variant Construction from Theoretical Foundation to Applications
• scientific article; zbMATH DE number 5033848 (Why is no real title available?)

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Variants of the basic calculus of constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1885480)