| No. |
Title |
Author |
Year |
| 1 |
Type Theory with Explicit Universe Polymorphism |
Bezem, Marc et al. |
2023 |
| 2 |
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472) |
Coquand, Thierry et al. |
2022 |
| 3 |
Verification and Constructive Algebra (Dagstuhl Seminar 03021) |
Coquand, Thierry et al. |
2021 |
| 4 |
Homotopy Canonicity for Cubical Type Theory |
Coquand, Thierry et al. |
2019 |
| 5 |
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic |
Adams, Robin et al. |
2018 |
| 6 |
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom |
Cohen, Cyril et al. |
2018 |
| 7 |
Realizability at Work: Separating Two Constructive Notions of Finiteness |
Bezem, Marc et al. |
2018 |
| 8 |
The Ackermann Award 2016 |
Coquand, Thierry et al. |
2016 |
| 9 |
The Independence of Markov’s Principle in Type Theory |
Coquand, Thierry et al. |
2016 |
| 10 |
Non-Constructivity in Kan Simplicial Sets |
Bezem, Marc et al. |
2015 |
| 11 |
A Model of Type Theory in Cubical Sets |
Bezem, Marc et al. |
2014 |
| 12 |
The Ackermann Award 2012 |
Coquand, Thierry et al. |
2012 |
| 13 |
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs |
Coquand, Thierry et al. |
2006 |
| 14 |
05021 Executive Summary -- Mathematics, Algorithms, Proofs |
Coquand, Thierry |
2006 |
| 15 |
A Nilregular Element Property |
Coquand, Thierry et al. |
2006 |
