Introducing the notion of inductive types in type theory
and with it the calculus of inductive constructions used by Coq:
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]
Christine Paulin-Mohring, Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) [hal:01094195, pdf, pdf slides]
Last revised on January 17, 2023 at 12:37:09. See the history of this page for a list of all contributions to it.