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

calculus of constructions pure typed systems typed \(\lambda\)-calculus

Mathematics Subject Classification ID

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

Review text

Different formulations of the calculus of constructions, introduced by Coquand in 1985, are compared. The different formulations have some things in common, namely the terms and forms of judgements, the axiom (just a single axiom for all the variants), and the form of the application and product rules. They may differ in the form of the rules for conversions of types, in the form of the abstraction rule, and in the structure imposed on assumptions (it could be a set or a sequence). If one has a purpose for which type-checking is important, one can follow the authors' argumentated advice and choose systems with assumptions-as-sequences in which abstraction and conversion are essentially those of pure typed systems or the abstraction rule is modified. At the same time, if one wants to obtain proof-theoretic results, one can use variants with assumptions-as-sets in which either the rule of conversion between types is modified or both abstraction and conversion rules are modified.

Recommendations

Cites work

Cited in

(2)

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)