nLab Christine Paulin-Mohring

• personal page

• Wikipedia entry

Selected writings

Introducing the notion of inductive types in type theory

• Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 [doi:10.1007/3-540-52335-9_47]

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]

category: people