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 homological algebra in constructive mathematics via type theory:
Discussion of notions of finite sets in constructive mathematics:
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:
On synthetic algebraic geometry:
Last revised on September 15, 2023 at 15:31:15. See the history of this page for a list of all contributions to it.