Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden.

Introducing the calculus of constructions that later forms the basis of the proof assistant *Coq*:

- Thierry Coquand, Gérard Huet,
*The Calculus of Constructions*, INRIA Rapport**530**(1986) [inria:00076024, pdf]

Introducing the notion of inductive types in type theory which later became the foundations of the calculus of inductive constructions used by Coq:

- 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]

On identity types in dependent type theory (homotopy type theory):

- Thierry Coquand, slides 26-28 of:
*Equality and dependent type theory*(2011) [pdf, pdf]

On the structure identity principle:

- Thierry Coquand, Nils Anders Danielsson,
*Isomorphism is equality*, Indagationes Mathematicae**24**4 (2013) 1105-1120 [doi:10.1016/j.indag.2013.09.002]

On weakly constant functions and propositional truncation in homotopy type theory:

- Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch,
*Notions of Anonymous Existence in Martin-Löf Type Theory*, Logical Methods in Computer Science**13**1 [doi:10.23638/LMCS-13(1:15)2017, arXiv:1610.03346]

category: people

Last revised on March 27, 2023 at 18:42:52. See the history of this page for a list of all contributions to it.