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

category: people

Last revised on May 24, 2024 at 05:25:35. See the history of this page for a list of all contributions to it.