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:
On projective spaces in synthetic algebraic geometry:
A constructive model of homotopy type theory in a Quillen model category of cubical sets that classically presents the usual homotopy theory of spaces:
Last revised on March 22, 2025 at 01:22:30. See the history of this page for a list of all contributions to it.