nLab Thierry Coquand

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

Selected writings

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

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

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

On the structure identity principle:

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

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.