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:
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:
Last revised on March 27, 2023 at 18:42:52. See the history of this page for a list of all contributions to it.