| 2026 | LICS | Constructive Higher Sheaf Models with Applications to Synthetic Mathematics. | Thierry Coquand, Jonas Hfer, Christian Sattler |
| 2018 | LICS | Inner Models of Univalence. | Thierry Coquand |
| 2018 | LICS | On Higher Inductive Types in Cubical Type Theory. | Thierry Coquand, Simon Huber, Anders Mrtberg |
| 2017 | CSR | Type Theory and Formalisation of Mathematics. | Thierry Coquand |
| 2017 | LICS | Stack semantics of type theory. | Thierry Coquand, Bassel Mannaa, Fabian Ruch |
| 2016 | CSL | The Ackermann Award 2016. | Thierry Coquand, Anuj Dawar |
| 2012 | CPP | Coherent and Strongly Discrete Rings in Type Theory. | Thierry Coquand, Anders Mrtberg, Vincent Siles |
| 2012 | CSL | The Ackermann Award 2012. | Thierry Coquand, Anuj Dawar, Damian Niwinski |
| 2012 | ITP | Stop When You Are Almost-Full - Adventures in Constructive Termination. | Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt |
| 2011 | CPP | A Decision Procedure for Regular Expression Equivalence in Type Theory. | Thierry Coquand, Vincent Siles |
| 2009 | CSL | Forcing and Type Theory. | Thierry Coquand |
| 2008 | ESOP | Constructive Mathematics and Functional Programming (Abstract). | Thierry Coquand |
| 2008 | FLOPS | On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. | Andreas Abel, Thierry Coquand, Peter Dybjer |
| 2008 | MPC | Verifying a Semantic beta-eta-Conversion Test for Martin-Lf Type Theory. | Andreas Abel, Thierry Coquand, Peter Dybjer |
| 2007 | LICS | Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. | Andreas Abel, Thierry Coquand, Peter Dybjer |
| 2006 | LICS | A Proof of Strong Normalisation using Domain Theory. | Thierry Coquand, Arnaud Spiwack |
| 2005 | CiE | A Logical Approach to Abstract Algebra. | Thierry Coquand |
| 2005 | LPAR | Automating Coherent Logic. | Marc Bezem, Thierry Coquand |
| 2003 | TABLEAUX | Dynamical Method in Algebra: A Survey. | Thierry Coquand |
| 2000 | CSL | Sequents, Frames, and Completeness. | Thierry Coquand, Guo-Qiang Zhang |
| 1997 | CSL | A Proof-Theoretical Investigation of Zantema's Problem. | Thierry Coquand, Henrik Persson |
| 1995 | MPC | Program Construction in Intuitionistic Type Theory (Abstract). | Thierry Coquand |
| 1989 | LICS | Inheritance and Explicit Coercion (Preliminary Report) | Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov |
| 1988 | LICS | Categories of Embeddings | Thierry Coquand |
| 1987 | MFPS | DI-Domains as a Model of Polymorphism. | Thierry Coquand, Carl A. Gunter, Glynn Winskel |
| 1986 | LICS | An Analysis of Girard's Paradox | Thierry Coquand |