natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
further
The Calculus of Constructions (CoC) is a type theory formal system for constructive proof in natural deduction style. This calculus goes back to Thierry Coquand and Gérard Huet
When supplemented by inductive types, it become the Calculus of Inductive Constructions (CIC). Sometimes coinductive types are included as well and one speaks of the Calculus of (co)inductive Constructions. This is what the Coq software implements.
More in detail, the Calculus of (co)Inductive Constructions is
a pure type system, hence
a system of natural deduction with dependent types;
with the natural-deduction rule for dependent product types specified;
with a rule for how to introduce new natural-deduction rules for arbitrary (co)inductive types.
and with universes:
a cumulative hierarchy of predicative types of types
and an impredicative type of propositions.
All of the other standard type formations are subsumed by the existence of arbitrary inductive types, notably the empty type, dependent sum types and identity types are special inductive types. Specifying these hence makes the calculus of constructions be an intensional dependent type theory.
Original articles:
Thierry Coquand, Gérard Huet, The Calculus of Constructions, INRIA Rapport 530 (1986) [inria:00076024, pdf]
Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) [doi:10.1007/BFb0037116]
(adding inductive types)
Review and surveys:
Zhaohui Luo, Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) ISBN:9780198538356, pdf
M. Bunder, Jonathan Seldin, Variants of the basic calculus of constructions, Journal of Applied Logic 2 2 (2004) 191-217 [doi:10.1016/j.jal.2004.02.004]
Christine Paulin-Mohring, Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) [hal:01094195, pdf, pdf slides]
Frade, Calculus of inductive constructions (pdf)
Wikipedia, Calculus of constructions
A categorical semantics for CoC is discussed in
For specifics of the implementation in Coq see
Historical references on the definition of inductive types.
A first type theoretic formulation of general inductive definitions:
The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:
and in the modern form of inference rules in:
The special case of inductive types now known as -types is first formulated in:
Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0
Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) pdf, pdf
Early proposals for a general formal definition of inductive types:
Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) doi:10.1007/3-540-15648-8_5
Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) hdl:1813/6710
Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) pdf, pdf
The modern notion of inductive types and inductive families in intensional type theory is independently due to
Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 doi:10.1017/CBO9780511569807.012, pdf
Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf
and due to
which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:
Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) doi:10.1007/BFb0040259
Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) doi:10.1007/BFb0037116
reviewed in
Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) ISBN:9780198538356, pdf
Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) hal:01094195, pdf, pdf slides
with streamlined exposition in:
The generalization to inductive-recursive types is due to
Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 doi:10.2307/2586554, pdf
Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) doi:10.1007/3-540-45504-3_7, pdf
See also:
Last revised on July 18, 2024 at 16:08:40. See the history of this page for a list of all contributions to it.