Constructions: A Higher Order Proof System for Mechanizing Mathematics. - Thierry Coquand; Gérard P. Huet (European Conference on Computer Algebra (1), 1985)

Sur l'Analogie entre les Propositions et les Types. - Thierry Coquand (Combinators and Functional Programming Languages, 1985)

Concepts mathématiques et informatiques formalisés dans le calcul des constructions. - Thierry Coquand; Gérard P. Huet (Logic Colloquium, 1985)

A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. - Thierry Coquand; Gérard P. Huet (J. Symb. Comput., 1985)

An Analysis of Girard's Paradox - Thierry Coquand (LICS, 1986)

An Equational Presentation of Higher Order Logic. - Thierry Coquand; Thomas Ehrhard (Category Theory and Computer Science, 1987)

DI-Domains as a Model of Polymorphism. - Thierry Coquand; Carl A. Gunter; Glynn Winskel (MFPS, 1987)

Inductively defined types. - Thierry Coquand; Christine Paulin (Conference on Computer Logic, 1988)

The Calculus of Constructions - Thierry Coquand; Gérard P. Huet (Inf. Comput., 1988)

Extensional Models for Polymorphism. - Val Tannen; Thierry Coquand (Theor. Comput. Sci., 1988)

Inheritance and Explicit Coercion (Preliminary Report) - Val Tannen; Thierry Coquand; Carl A. Gunter; Andre Scedrov (LICS, 1989)

Categories of Embeddings. - Thierry Coquand (Theor. Comput. Sci., 1989)

Domain Theoretic Models of Polymorphism - Thierry Coquand; Carl A. Gunter; Glynn Winskel (Inf. Comput., 1989)

Constructive Topology and Combinatorics. - Thierry Coquand (Constructivity in Computer Science, 1991)

A Direct Proof of the Intuitionistic Ramsey Theorem. - Thierry Coquand (Category Theory and Computer Science, 1991)

Inheritance as Implicit Coercion - Val Tannen; Thierry Coquand; Carl A. Gunter; Andre Scedrov (Inf. Comput., 1991)

The Paradox of Trees in Type Theory. - Thierry Coquand (BIT, 1992)

An Intuitionistic Proof of Tychonoff's Theorem. - Thierry Coquand (J. Symb. Log., 1992)

Infinite Objects in Type Theory. - Thierry Coquand (TYPES, 1993)

Another Proof of the Intuitionistic Ramsey Theorem. - Thierry Coquand (Theor. Comput. Sci., 1993)

Inductive Definitions and Type Theory: an Introduction (Preliminary Version). - Thierry Coquand; Peter Dybjer (FSTTCS, 1994)

Type Theorie Programming. - Thierry Coquand; Bengt Nordström; Jan M. Smith; Björn von Sydow (Bull. EATCS, 1994)

A - Translation and Looping Combinators in Pure Type Systems. - Thierry Coquand; Hugo Herbelin (J. Funct. Program., 1994)

An Analysis of Ramsey's Theorem - Thierry Coquand (Inf. Comput., 1994)

Program Construction in Intuitionistic Type Theory (Abstract). - Thierry Coquand (MPC, 1995)

A realization of the negative interpretation of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (TLCA, 1995)

An Application of Constructive Completeness. - Thierry Coquand; Jan M. Smith (TYPES, 1995)

A Semantics of Evidence for Classical Arithmetic. - Thierry Coquand (J. Symb. Log., 1995)

An Algorithm for Type-Checking Dependent Types. - Thierry Coquand (Sci. Comput. Program., 1996)

A Proof-Theoretical Investigation of Zantema's Problem. - Thierry Coquand; Henrik Persson (CSL, 1997)

Minimal Invariant Spaces in Formal Topology. - Thierry Coquand (J. Symb. Log., 1997)

Intuitionistic Model Constructions and Normalization Proofs. - Thierry Coquand; Peter Dybjer (Math. Struct. Comput. Sci., 1997)

Gröbner Bases in Type Theory. - Thierry Coquand; Henrik Persson (TYPES, 1998)

Two applications of Boolean models. - Thierry Coquand (Arch. Math. Log., 1998)

A Note on Formal Iterated Function Systems. - Thierry Coquand (RealComp, 1998)

On the Computational Content of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (J. Symb. Log., 1998)

A Boolean Model of Ultrafilters. - Thierry Coquand (Ann. Pure Appl. Log., 1999)

A new method for establishing conservativity of classical systems over their intuitionistic version. - Thierry Coquand; Martin Hofmann 001 (Math. Struct. Comput. Sci., 1999)

An Introduction to Dependent Type Theory. - Gilles Barthe; Thierry Coquand (APPSEM, 2000)

Sequents, Frames, and Completeness. - Thierry Coquand; Guo-Qiang Zhang 001 (CSL, 2000)

An Implementation of Type: Type. - Thierry Coquand; Makoto Takeyama (TYPES, 2000)

Intuitionistic choice and classical logic. - Thierry Coquand; Erik Palmgren (Arch. Math. Log., 2000)

Formal Topologies on The Set of First-Order Formulae. - Thierry Coquand; Sara Sadocco; Giovanni Sambin; Jan M. Smith (J. Symb. Log., 2000)

A Finitary Subsystem of the Polymorphic lambda-Calculus. - Thorsten Altenkirch; Thierry Coquand (TLCA, 2001)

Metric Boolean algebras and constructive measure theory. - Thierry Coquand; Erik Palmgren (Arch. Math. Log., 2002)

Dynamical Method in Algebra: A Survey. - Thierry Coquand (TABLEAUX, 2003)

Inductively generated formal topologies. - Thierry Coquand; Giovanni Sambin; Jan M. Smith; Silvio Valentini (Ann. Pure Appl. Log., 2003)

Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. - Marc Bezem; Thierry Coquand (Bull. EATCS, 2003)

A syntactical proof of the Marriage Lemma. - Thierry Coquand (Theor. Comput. Sci., 2003)

A representation of stably compact spaces, and patch topology. - Thierry Coquand; Guo-Qiang Zhang 001 (Theor. Comput. Sci., 2003)

Formalising Bitonic Sort in Type Theory. - Ana Bove; Thierry Coquand (TYPES, 2004)

Proof-theoretical analysis of order relations. - Sara Negri; Jan von Plato; Thierry Coquand (Arch. Math. Log., 2004)

An elementary characterisation of Krull dimension. - Thierry Coquand; Henri Lombardi; Marie-Françoise Roy (From sets and types to topology and analysis, 2005)

A Logical Approach to Abstract Algebra. - Thierry Coquand (CiE, 2005)

05021 Executive Summary – Mathematics, Algorithms, Proofs. - Thierry Coquand (Mathematics, Algorithms, Proofs, 2005)

05021 Abstracts Collection – Mathematics, Algorithms, Proofs. - Thierry Coquand; Henri Lombardi; Marie-Françoise Roy (Mathematics, Algorithms, Proofs, 2005)

A Nilregular Element Property. - Thierry Coquand; Henri Lombardi; Peter Schuster 001 (Mathematics, Algorithms, Proofs, 2005)

Connecting a Logical Framework to a First-Order Logic Prover. - Andreas Abel 001; Thierry Coquand; Ulf Norell (FroCoS, 2005)

Automating Coherent Logic. - Marc Bezem; Thierry Coquand (LPAR, 2005)

Completeness Theorems and lambda-Calculus. - Thierry Coquand (TLCA, 2005)

A Logical Framework with Dependently Typed Records. - Thierry Coquand; Randy Pollack; Makoto Takeyama (Fundam. Informaticae, 2005)

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. - Thierry Coquand; Bas Spitters (J. Univers. Comput. Sci., 2005)

A constructive proof of the Peter-Weyl theorem. - Thierry Coquand; Bas Spitters (Math. Log. Q., 2005)

A Short Proof for the Krull Dimension of a Polynomial Ring. - Thierry Coquand; Henri Lombardi (Am. Math. Mon., 2005)

Alfa/Agda. - Thierry Coquand (The Seventeen Provers of the World, 2006)

Preface. - Bernhard Banaschewski; Thierry Coquand; Giovanni Sambin (Ann. Pure Appl. Log., 2006)

Remarks on the equational theory of non-normalizing pure type systems. - Gilles Barthe; Thierry Coquand (J. Funct. Program., 2006)

A logical approach to abstract algebra. - Thierry Coquand; Henri Lombardi (Math. Struct. Comput. Sci., 2006)

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (LICS, 2007)

Towards Constructive Homological Algebra in Type Theory. - Thierry Coquand; Arnaud Spiwack (Calculemus/MKM, 2007)

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. - Andreas Abel 001; Thierry Coquand (Fundam. Informaticae, 2007)

The Completeness of Typing for Context-Semantics. - Thierry Coquand (Fundam. Informaticae, 2007)

A proof of strong normalisation using domain theory. - Thierry Coquand; Arnaud Spiwack (Log. Methods Comput. Sci., 2007)

Constructive Mathematics and Functional Programming (Abstract). - Thierry Coquand (ESOP, 2008)

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (FLOPS, 2008)

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (MPC, 2008)

A note on the axiomatisation of real numbers. - Thierry Coquand; Henri Lombardi (Math. Log. Q., 2008)

Forcing and Type Theory. - Thierry Coquand (CSL, 2009)

Spectral schemes as ringed lattices. - Thierry Coquand; Henri Lombardi; Peter Schuster 001 (Ann. Math. Artif. Intell., 2009)

Space of valuations. - Thierry Coquand (Ann. Pure Appl. Log., 2009)

Integrals and valuations. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2009)

Games with 1-backtracking. - Stefano Berardi; Thierry Coquand; Susumu Hayashi (Ann. Pure Appl. Log., 2010)

A Note on Forcing and Type Theory. - Thierry Coquand; Guilhem Jaber (Fundam. Informaticae, 2010)

Constructive theory of Banach algebras. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2010)

Curves and coherent Prüfer rings. - Thierry Coquand; Henri Lombardi; Claude Quitté (J. Symb. Comput., 2010)

A Decision Procedure for Regular Expression Equivalence in Type Theory. - Thierry Coquand; Vincent Siles (CPP, 2011)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance - Andreas Abel 001; Thierry Coquand; Miguel Pagano (Log. Methods Comput. Sci., 2011)

Unique paths as formal points. - Thierry Coquand; Peter Schuster 001 (J. Log. Anal., 2011)

Metric complements of overt closed sets. - Thierry Coquand; Erik Palmgren; Bas Spitters (Math. Log. Q., 2011)

Coherent and Strongly Discrete Rings in Type Theory. - Thierry Coquand; Anders Mörtberg; Vincent Siles (CPP, 2012)

The Ackermann Award 2012. - Thierry Coquand; Anuj Dawar; Damian Niwinski (CSL, 2012)

Stop When You Are Almost-Full - Adventures in Constructive Termination. - Dimitrios Vytiniotis; Thierry Coquand; David Wahlstedt (ITP, 2012)

Preface. - Andrej Bauer; Thierry Coquand; Giovanni Sambin; Peter M. Schuster (Ann. Pure Appl. Log., 2012)

A formal proof of Sasaki-Murao algorithm. - Thierry Coquand; Anders Mörtberg; Vincent Siles (J. Formaliz. Reason., 2012)

A constructive proof of Simpson's Rule. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2012)

A Computational Interpretation of Forcing in Type Theory. - Thierry Coquand; Guilhem Jaber (Epistemology versus Ontology, 2012)

Generalizations of Hedberg's Theorem. - Nicolai Kraus; Martín Hötzel Escardó; Thierry Coquand; Thorsten Altenkirch (TLCA, 2013)

A Model of Type Theory in Cubical Sets. - Marc Bezem; Thierry Coquand; Simon Huber (TYPES, 2013)

About Goodman's Theorem. - Thierry Coquand (Ann. Pure Appl. Log., 2013)

Dynamic Newton-Puiseux theorem. - Bassel Mannaa; Thierry Coquand (J. Log. Anal., 2013)

Computing persistent homology within Coq/SSReflect. - Jónathan Heras; Thierry Coquand; Anders Mörtberg; Vincent Siles (ACM Trans. Comput. Log., 2013)

A Sheaf Model of the Algebraic Closure. - Bassel Mannaa; Thierry Coquand (CL&C, 2014)

Non-Constructivity in Kan Simplicial Sets. - Marc Bezem; Thierry Coquand; Erik Parmann (TLCA, 2015)

A Presheaf Model of Parametric Type Theory. - Jean-Philippe Bernardy; Thierry Coquand; Guilhem Moulin (MFPS, 2015)

A generalization of the Takeuti-Gandy interpretation. - Bruno Barras; Thierry Coquand; Simon Huber (Math. Struct. Comput. Sci., 2015)

A Kripke model for simplicial sets. - Marc Bezem; Thierry Coquand (Theor. Comput. Sci., 2015)

The Ackermann Award 2016. - Thierry Coquand; Anuj Dawar (CSL, 2016)

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. - Robin Adams 001; Marc Bezem; Thierry Coquand (TYPES, 2016)

Realizability at Work: Separating Two Constructive Notions of Finiteness. - Marc Bezem; Thierry Coquand; Keiko Nakata 001; Erik Parmann (TYPES, 2016)

Preface. - Thierry Coquand; Maria Emilia Maietti; Giovanni Sambin; Peter Schuster 001 (Ann. Pure Appl. Log., 2016)

A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. - Robin Adams 001; Marc Bezem; Thierry Coquand (CoRR, 2016)

Type Theory and Formalisation of Mathematics. - Thierry Coquand (CSR, 2017)

Stack semantics of type theory. - Thierry Coquand; Bassel Mannaa; Fabian Ruch (LICS, 2017)

Notions of Anonymous Existence in Martin-Löf Type Theory. - Nicolai Kraus; Martín Escardó; Thierry Coquand; Thorsten Altenkirch (Log. Methods Comput. Sci., 2017)

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. - Cyril Cohen; Thierry Coquand; Simon Huber; Anders Mörtberg (FLAP, 2017)

The Independence of Markov's Principle in Type Theory. - Thierry Coquand; Bassel Mannaa (Log. Methods Comput. Sci., 2017)

Inner Models of Univalence. - Thierry Coquand (LICS, 2018)

On Higher Inductive Types in Cubical Type Theory. - Thierry Coquand; Simon Huber; Anders Mörtberg (LICS, 2018)

Canonicity and normalisation for Dependent Type Theory. - Thierry Coquand (CoRR, 2018)

A survey of constructive presheaf models of univalence. - Thierry Coquand (ACM SIGLOG News, 2018)

Homotopy Canonicity for Cubical Type Theory. - Thierry Coquand; Simon Huber; Christian Sattler (FSCD, 2019)

Skolem's Theorem in Coherent Logic. - Marc Bezem; Thierry Coquand (Fundam. Informaticae, 2019)

The Univalence Axiom in Cubical Sets. - Marc Bezem; Thierry Coquand; Simon Huber (J. Autom. Reason., 2019)

Preface to the special issue for The Fifth Workshop on Formal Topology. - Thierry Coquand; Maria Emilia Maietti; Erik Palmgren (J. Log. Anal., 2019)

An Adequacy Theorem for Dependent Type Theory. - Thierry Coquand; Simon Huber (Theory Comput. Syst., 2019)

Canonicity and normalization for dependent type theory. - Thierry Coquand (Theor. Comput. Sci., 2019)

A Note on Generalized Algebraic Theories and Categories with Families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2020)

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. - Andreas Abel 001; Thierry Coquand (Log. Methods Comput. Sci., 2020)

Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). - Thierry Coquand; Hajime Ishihara; Sara Negri; Peter M. Schuster (Dagstuhl Reports, 2021)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

On generalized algebraic theories and categories with families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (Math. Struct. Comput. Sci., 2021)

Constructive sheaf models of type theory. - Thierry Coquand; Fabian Ruch; Christian Sattler (Math. Struct. Comput. Sci., 2021)

Type Theory with Explicit Universe Polymorphism. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (TYPES, 2022)

Controlling unfolding in type theory. - Daniel Gratzer; Jonathan Sterling; Carlo Angiuli; Thierry Coquand; Lars Birkedal (CoRR, 2022)

Type Theories with Universe Level Judgements. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2022)

Canonicity and homotopy canonicity for cubical type theory. - Thierry Coquand; Simon Huber; Christian Sattler (Log. Methods Comput. Sci., 2022)

Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. - Marc Bezem; Thierry Coquand (Theor. Comput. Sci., 2022)

Reduction Free Normalisation for a proof irrelevant type of propositions. - Thierry Coquand (Log. Methods Comput. Sci., 2023)

Some Remarks About Dependent Type Theory. - Thierry Coquand (The French School of Programming, 2024)

A Variation of Reynolds-Hurkens Paradox. - Thierry Coquand (Logics and Type Systems in Theory and Practice, 2024)

A Foundation for Synthetic Stone Duality. - Felix Cherubini; Thierry Coquand; Freek Geerligs; Hugo Moeneclaey (TYPES, 2024)

The equivariant model structure on cartesian cubical sets. - Steve Awodey; Evan Cavallo; Thierry Coquand; Emily Riehl; Christian Sattler (CoRR, 2024)

A foundation for synthetic algebraic geometry. - Felix Cherubini; Thierry Coquand; Matthias Hutzler (Math. Struct. Comput. Sci., 2024)