Variants of the basic calculus of constructions (Q1885480)

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.