Thierry Coquand

ORCID

Publication Activity (10 Years)

Years Active: 1985-2024
Publications (10 Years): 44

Top Venues

CoRR

Log. Methods Comput. Sci.

Math. Struct. Comput. Sci.

TYPES

Publications

Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, Christian Sattler
The equivariant model structure on cartesian cubical sets. CoRR (2024)
Thierry Coquand
A Variation of Reynolds-Hurkens Paradox. Logics and Type Systems in Theory and Practice (2024)
Thierry Coquand
A variation of Reynolds-Hurkens Paradox. CoRR (2023)
Thierry Coquand
Reduction Free Normalisation for a proof irrelevant type of propositions. Log. Methods Comput. Sci. 19 (3) (2023)
Marc Bezem, Thierry Coquand
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theor. Comput. Sci. 913 (2022)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
Controlling unfolding in type theory. CoRR (2022)
Thierry Coquand, Simon Huber, Christian Sattler
Canonicity and homotopy canonicity for cubical type theory. Log. Methods Comput. Sci. 18 (1) (2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
Type Theories with Universe Level Judgements. CoRR (2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
Type Theory with Explicit Universe Polymorphism. TYPES (2022)
Thierry Coquand, Hajime Ishihara, Sara Negri, Peter M. Schuster
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). Dagstuhl Reports 11 (10) (2021)
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31 (4) (2021)
Thierry Coquand, Fabian Ruch, Christian Sattler
Constructive sheaf models of type theory. Math. Struct. Comput. Sci. 31 (9) (2021)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. 31 (9) (2021)
Thierry Coquand
Reduction Free Normalisation for a proof irrelevant type of propositions. CoRR (2021)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
A Note on Generalized Algebraic Theories and Categories with Families. CoRR (2020)
Andreas Abel, Thierry Coquand
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Log. Methods Comput. Sci. 16 (2) (2020)
Andreas Abel, Thierry Coquand
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. CoRR (2019)
Thierry Coquand, Maria Emilia Maietti, Erik Palmgren
Preface to the special issue for The Fifth Workshop on Formal Topology. J. Log. Anal. 11 (2019)
Thierry Coquand, Simon Huber, Christian Sattler
Homotopy Canonicity for Cubical Type Theory. FSCD (2019)
Thierry Coquand, Simon Huber, Christian Sattler
Homotopy canonicity for cubical type theory. CoRR (2019)
Marc Bezem, Thierry Coquand
Skolem's Theorem in Coherent Logic. Fundam. Informaticae 170 (1-3) (2019)
Marc Bezem, Thierry Coquand, Simon Huber
The Univalence Axiom in Cubical Sets. J. Autom. Reason. 63 (2) (2019)
Thierry Coquand
Canonicity and normalization for dependent type theory. Theor. Comput. Sci. 777 (2019)
Thierry Coquand, Simon Huber
An Adequacy Theorem for Dependent Type Theory. Theory Comput. Syst. 63 (4) (2019)
Thierry Coquand, Simon Huber, Anders Mörtberg
On Higher Inductive Types in Cubical Type Theory. LICS (2018)
Thierry Coquand, Simon Huber, Anders Mörtberg
On Higher Inductive Types in Cubical Type Theory. CoRR (2018)
Thierry Coquand
A survey of constructive presheaf models of univalence. ACM SIGLOG News 5 (3) (2018)
Thierry Coquand
Inner Models of Univalence. LICS (2018)
Thierry Coquand
Canonicity and normalisation for Dependent Type Theory. CoRR (2018)
Thierry Coquand, Bassel Mannaa, Fabian Ruch
Stack semantics of type theory. LICS (2017)
Thierry Coquand, Bassel Mannaa, Fabian Ruch
Stack Semantics of Type Theory. CoRR (2017)
Marc Bezem, Thierry Coquand, Simon Huber
The univalence axiom in cubical sets. CoRR (2017)
Thierry Coquand
Type Theory and Formalisation of Mathematics. CSR (2017)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4 (10) (2017)
Thierry Coquand, Bassel Mannaa
The Independence of Markov's Principle in Type Theory. Log. Methods Comput. Sci. 13 (3) (2017)
Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
Notions of Anonymous Existence in Martin-Löf Type Theory. Log. Methods Comput. Sci. 13 (1) (2017)
Robin Adams, Marc Bezem, Thierry Coquand
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. TYPES (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR (2016)
Thierry Coquand, Bassel Mannaa
The Independence of Markov's Principle in Type Theory. FSCD (2016)
Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann
Realizability at Work: Separating Two Constructive Notions of Finiteness. TYPES (2016)
Robin Adams, Marc Bezem, Thierry Coquand
A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR (2016)
Thierry Coquand, Anuj Dawar
The Ackermann Award 2016. CSL (2016)
Thierry Coquand, Bassel Mannaa
The Independence of Markov's Principle in Type Theory. CoRR (2016)
Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin, Peter Schuster
Preface. Ann. Pure Appl. Log. 167 (9) (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. TYPES (2015)
Marc Bezem, Thierry Coquand
A Kripke model for simplicial sets. Theor. Comput. Sci. 574 (2015)
Marc Bezem, Thierry Coquand, Erik Parmann
Non-Constructivity in Kan Simplicial Sets. TLCA (2015)
Bruno Barras, Thierry Coquand, Simon Huber
A generalization of the Takeuti-Gandy interpretation. Math. Struct. Comput. Sci. 25 (5) (2015)
Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
A Presheaf Model of Parametric Type Theory. MFPS (2015)
Bassel Mannaa, Thierry Coquand
A Sheaf Model of the Algebraic Closure. CL&C (2014)
Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch
Generalizations of Hedberg's Theorem. TLCA (2013)
Bassel Mannaa, Thierry Coquand
Dynamic Newton-Puiseux theorem. J. Log. Anal. 5 (2013)
Marc Bezem, Thierry Coquand, Simon Huber
A Model of Type Theory in Cubical Sets. TYPES (2013)
Thierry Coquand
About Goodman's Theorem. Ann. Pure Appl. Log. 164 (4) (2013)
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14 (4) (2013)
Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster
Preface. Ann. Pure Appl. Log. 163 (2) (2012)
Thierry Coquand, Anders Mörtberg, Vincent Siles
Coherent and Strongly Discrete Rings in Type Theory. CPP (2012)
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
Computing Persistent Homology within Coq/SSReflect CoRR (2012)
Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt
Stop When You Are Almost-Full - Adventures in Constructive Termination. ITP (2012)
Thierry Coquand, Anuj Dawar, Damian Niwinski
The Ackermann Award 2012. CSL (2012)
Thierry Coquand, Bas Spitters
A constructive proof of Simpson's Rule. J. Log. Anal. 4 (2012)
Thierry Coquand, Anders Mörtberg, Vincent Siles
A formal proof of Sasaki-Murao algorithm. J. Formaliz. Reason. 5 (1) (2012)
Thierry Coquand, Peter Schuster
Unique paths as formal points. J. Log. Anal. 3 (2011)
Thierry Coquand, Vincent Siles
A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP (2011)
Andreas Abel, Thierry Coquand, Miguel Pagano
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance Log. Methods Comput. Sci. 7 (2) (2011)
Thierry Coquand, Erik Palmgren, Bas Spitters
Metric complements of overt closed sets. Math. Log. Q. 57 (4) (2011)
Stefano Berardi, Thierry Coquand, Susumu Hayashi
Games with 1-backtracking. Ann. Pure Appl. Log. 161 (10) (2010)
Thierry Coquand, Henri Lombardi, Claude Quitté
Curves and coherent Prüfer rings. J. Symb. Comput. 45 (12) (2010)
Thierry Coquand, Guilhem Jaber
A Note on Forcing and Type Theory. Fundam. Informaticae 100 (1-4) (2010)
Thierry Coquand, Bas Spitters
Constructive theory of Banach algebras. J. Log. Anal. 2 (2010)
Thierry Coquand, Bas Spitters
Integrals and valuations. J. Log. Anal. 1 (2009)
Thierry Coquand, Henri Lombardi, Peter Schuster
Spectral schemes as ringed lattices. Ann. Math. Artif. Intell. 56 (3-4) (2009)
Andreas Abel, Thierry Coquand, Miguel Pagano
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA (2009)
Thierry Coquand
Space of valuations. Ann. Pure Appl. Log. 157 (2-3) (2009)
Thierry Coquand
Forcing and Type Theory. CSL (2009)
Thierry Coquand, Henri Lombardi
A note on the axiomatisation of real numbers. Math. Log. Q. 54 (3) (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC (2008)
Thierry Coquand
Constructive Mathematics and Functional Programming (Abstract). ESOP (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS (2007)
Thierry Coquand
The Completeness of Typing for Context-Semantics. Fundam. Informaticae 77 (4) (2007)
Thierry Coquand, Arnaud Spiwack
A proof of strong normalisation using domain theory CoRR (2007)
Thierry Coquand, Arnaud Spiwack
A proof of strong normalisation using domain theory. Log. Methods Comput. Sci. 3 (4) (2007)
Thierry Coquand, Arnaud Spiwack
Towards Constructive Homological Algebra in Type Theory. Calculemus/MKM (2007)
Andreas Abel, Thierry Coquand
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Informaticae 77 (4) (2007)
Bernhard Banaschewski, Thierry Coquand, Giovanni Sambin
Preface. Ann. Pure Appl. Log. 137 (1-3) (2006)
Thierry Coquand, Henri Lombardi
A logical approach to abstract algebra. Math. Struct. Comput. Sci. 16 (5) (2006)
Thierry Coquand, Arnaud Spiwack
A Proof of Strong Normalisation using Domain Theory. LICS (2006)
Gilles Barthe, Thierry Coquand
Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16 (2) (2006)
Andreas Abel, Thierry Coquand
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA (2005)
Thierry Coquand
Completeness Theorems and lambda-Calculus. TLCA (2005)
Thierry Coquand, Henri Lombardi, Marie-Françoise Roy
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs (2005)
Thierry Coquand, Henri Lombardi, Peter Schuster
A Nilregular Element Property. Mathematics, Algorithms, Proofs (2005)
Thierry Coquand, Bas Spitters
A constructive proof of the Peter-Weyl theorem. Math. Log. Q. 51 (4) (2005)
Thierry Coquand
05021 Executive Summary -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs (2005)
Thierry Coquand, Bas Spitters
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. Univers. Comput. Sci. 11 (12) (2005)
Thierry Coquand, Randy Pollack, Makoto Takeyama
A Logical Framework with Dependently Typed Records. Fundam. Informaticae 65 (1-2) (2005)
Andreas Abel, Thierry Coquand, Ulf Norell
Connecting a Logical Framework to a First-Order Logic Prover. FroCoS (2005)
Stefano Berardi, Thierry Coquand, Susumu Hayashi
Games with 1-backtracking. GALOP@ETAPS (2005)
Marc Bezem, Thierry Coquand
Automating Coherent Logic. LPAR (2005)

Thierry Coquand.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Thierry Coquand