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):
Early discussion of cubical type theory with categorical semantics in cubical sets:
Marc Bezem, Thierry Coquand, Simon Huber: A Model of Type Theory in Cubical Sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013) [doi:10.4230/LIPIcs.TYPES.2013.107, pdf]
Marc Bezem, Thierry Coquand, Simon Huber: The univalence axiom in cubical sets, Journal of Automated Reasoning 63 (2019) [doi:10.1007/s10817-018-9472-6, arXiv:1710.10941]
On the structure identity principle:
On weakly constant functions and propositional truncation in homotopy type theory:
On homotopy canonicity for cubical type theory:
Thierry Coquand, Simon Huber, Christian Sattler: Homotopy canonicity for cubical type theory, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) [doi:10.4230/LIPIcs.FSCD.2019.11, arXiv:1902.06572]
Thierry Coquand, Simon Huber, Christian Sattler: Canonicity and homotopy canonicity for cubical type theory, Logical Methods in Computer Science 18 1 (2022) lmcs:9043 [doi:10.46298/lmcs-18%281%3A28%292022, arXiv:1902.06572]
On formal topology via homotopy type theory:
On synthetic algebraic geometry:
On projective spaces in synthetic algebraic geometry:
On Châtelet’s theorem 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 April 17, 2026 at 19:45:11. See the history of this page for a list of all contributions to it.