Thierry Coquand

168 papers A* 8A 1B 16C 1Misc 2Journal 96Unranked 38

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2026	J	`jnl`	Two Remarks about Game Semantics of Classical Logic. CoRR Thierry Coquand
2025	J	`jnl`	Controlling unfolding in type theory. Math. Struct. Comput. Sci. Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2024	—	`conf`	A Foundation for Synthetic Stone Duality. TYPES Felix Cherubini, Thierry Coquand, Freek Geerligs, Hugo Moeneclaey
2024	—	`conf`	A Variation of Reynolds-Hurkens Paradox. Logics and Type Systems in Theory and Practice Thierry Coquand
2024	J	`jnl`	A foundation for synthetic algebraic geometry. Math. Struct. Comput. Sci. Felix Cherubini, Thierry Coquand, Matthias Hutzler
2024	—	`ch.`	Some Remarks About Dependent Type Theory. The French School of Programming Thierry Coquand
2024	J	`jnl`	The equivariant model structure on cartesian cubical sets. CoRR Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, Christian Sattler
2023	J	`jnl`	A variation of Reynolds-Hurkens Paradox. CoRR Thierry Coquand
2023	J	`jnl`	Reduction Free Normalisation for a proof irrelevant type of propositions. Log. Methods Comput. Sci. Thierry Coquand
2022	J	`jnl`	Canonicity and homotopy canonicity for cubical type theory. Log. Methods Comput. Sci. Thierry Coquand, Simon Huber, Christian Sattler
2022	J	`jnl`	Controlling unfolding in type theory. CoRR Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2022	J	`jnl`	Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theor. Comput. Sci. Marc Bezem, Thierry Coquand
2022	J	`jnl`	Type Theories with Universe Level Judgements. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2022	—	`conf`	Type Theory with Explicit Universe Polymorphism. TYPES Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2021	J	`jnl`	Constructive sheaf models of type theory. Math. Struct. Comput. Sci. Thierry Coquand, Fabian Ruch, Christian Sattler
2021	J	`jnl`	Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). Dagstuhl Reports Thierry Coquand, Hajime Ishihara, Sara Negri, Peter M. Schuster
2021	J	`jnl`	On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2021	J	`jnl`	Reduction Free Normalisation for a proof irrelevant type of propositions. CoRR Thierry Coquand
2021	J	`jnl`	Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
2020	J	`jnl`	A Note on Generalized Algebraic Theories and Categories with Families. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2020	J	`jnl`	Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Log. Methods Comput. Sci. Andreas Abel, Thierry Coquand
2019	J	`jnl`	An Adequacy Theorem for Dependent Type Theory. Theory Comput. Syst. Thierry Coquand, Simon Huber
2019	J	`jnl`	Canonicity and normalization for dependent type theory. Theor. Comput. Sci. Thierry Coquand
2019	J	`jnl`	Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. CoRR Andreas Abel, Thierry Coquand
2019	B	`conf`	Homotopy Canonicity for Cubical Type Theory. FSCD Thierry Coquand, Simon Huber, Christian Sattler
2019	J	`jnl`	Homotopy canonicity for cubical type theory. CoRR Thierry Coquand, Simon Huber, Christian Sattler
2019	J	`jnl`	Preface to the special issue for The Fifth Workshop on Formal Topology. J. Log. Anal. Thierry Coquand, Maria Emilia Maietti, Erik Palmgren
2019	J	`jnl`	Skolem's Theorem in Coherent Logic. Fundam. Informaticae Marc Bezem, Thierry Coquand
2019	J	`jnl`	The Univalence Axiom in Cubical Sets. J. Autom. Reason. Marc Bezem, Thierry Coquand, Simon Huber
2018	J	`jnl`	A survey of constructive presheaf models of univalence. ACM SIGLOG News Thierry Coquand
2018	J	`jnl`	Canonicity and normalisation for Dependent Type Theory. CoRR Thierry Coquand
2018	A*	`conf`	Inner Models of Univalence. LICS Thierry Coquand
2018	A*	`conf`	On Higher Inductive Types in Cubical Type Theory. LICS Thierry Coquand, Simon Huber, Anders Mörtberg
2018	J	`jnl`	On Higher Inductive Types in Cubical Type Theory. CoRR Thierry Coquand, Simon Huber, Anders Mörtberg
2017	J	`jnl`	Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
2017	J	`jnl`	Notions of Anonymous Existence in Martin-Löf Type Theory. Log. Methods Comput. Sci. Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
2017	J	`jnl`	Stack Semantics of Type Theory. CoRR Thierry Coquand, Bassel Mannaa, Fabian Ruch
2017	A*	`conf`	Stack semantics of type theory. LICS Thierry Coquand, Bassel Mannaa, Fabian Ruch
2017	J	`jnl`	The Independence of Markov's Principle in Type Theory. Log. Methods Comput. Sci. Thierry Coquand, Bassel Mannaa
2017	J	`jnl`	The univalence axiom in cubical sets. CoRR Marc Bezem, Thierry Coquand, Simon Huber
2017	Misc	`conf`	Type Theory and Formalisation of Mathematics. CSR Thierry Coquand
2016	—	`conf`	A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. TYPES Robin Adams, Marc Bezem, Thierry Coquand
2016	J	`jnl`	A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR Robin Adams, Marc Bezem, Thierry Coquand
2016	J	`jnl`	Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
2016	J	`jnl`	Preface. Ann. Pure Appl. Log. Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin, Peter Schuster
2016	—	`conf`	Realizability at Work: Separating Two Constructive Notions of Finiteness. TYPES Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann
2016	B	`conf`	The Ackermann Award 2016. CSL Thierry Coquand, Anuj Dawar
2016	B	`conf`	The Independence of Markov's Principle in Type Theory. FSCD Thierry Coquand, Bassel Mannaa
2016	J	`jnl`	The Independence of Markov's Principle in Type Theory. CoRR Thierry Coquand, Bassel Mannaa
2015	J	`jnl`	A Kripke model for simplicial sets. Theor. Comput. Sci. Marc Bezem, Thierry Coquand
2015	B	`conf`	A Presheaf Model of Parametric Type Theory. MFPS Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
2015	J	`jnl`	A generalization of the Takeuti-Gandy interpretation. Math. Struct. Comput. Sci. Bruno Barras, Thierry Coquand, Simon Huber
2015	—	`conf`	Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. TYPES Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
2015	—	`conf`	Non-Constructivity in Kan Simplicial Sets. TLCA Marc Bezem, Thierry Coquand, Erik Parmann
2014	—	`conf`	A Sheaf Model of the Algebraic Closure. CL&C Bassel Mannaa, Thierry Coquand
2013	—	`conf`	A Model of Type Theory in Cubical Sets. TYPES Marc Bezem, Thierry Coquand, Simon Huber
2013	J	`jnl`	About Goodman's Theorem. Ann. Pure Appl. Log. Thierry Coquand
2013	J	`jnl`	Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
2013	J	`jnl`	Dynamic Newton-Puiseux theorem. J. Log. Anal. Bassel Mannaa, Thierry Coquand
2013	—	`conf`	Generalizations of Hedberg's Theorem. TLCA Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch
2012	—	`ch.`	A Computational Interpretation of Forcing in Type Theory. Epistemology versus Ontology Thierry Coquand, Guilhem Jaber
2012	J	`jnl`	A constructive proof of Simpson's Rule. J. Log. Anal. Thierry Coquand, Bas Spitters
2012	J	`jnl`	A formal proof of Sasaki-Murao algorithm. J. Formaliz. Reason. Thierry Coquand, Anders Mörtberg, Vincent Siles
2012	B	`conf`	Coherent and Strongly Discrete Rings in Type Theory. CPP Thierry Coquand, Anders Mörtberg, Vincent Siles
2012	J	`jnl`	Computing Persistent Homology within Coq/SSReflect CoRR Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
2012	J	`jnl`	Preface. Ann. Pure Appl. Log. Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster
2012	B	`conf`	Stop When You Are Almost-Full - Adventures in Constructive Termination. ITP Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt
2012	B	`conf`	The Ackermann Award 2012. CSL Thierry Coquand, Anuj Dawar, Damian Niwinski
2011	B	`conf`	A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP Thierry Coquand, Vincent Siles
2011	J	`jnl`	A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance Log. Methods Comput. Sci. Andreas Abel, Thierry Coquand, Miguel Pagano
2011	J	`jnl`	Metric complements of overt closed sets. Math. Log. Q. Thierry Coquand, Erik Palmgren, Bas Spitters
2011	J	`jnl`	Unique paths as formal points. J. Log. Anal. Thierry Coquand, Peter Schuster
2010	J	`jnl`	A Note on Forcing and Type Theory. Fundam. Informaticae Thierry Coquand, Guilhem Jaber
2010	J	`jnl`	Constructive theory of Banach algebras. J. Log. Anal. Thierry Coquand, Bas Spitters
2010	J	`jnl`	Curves and coherent Prüfer rings. J. Symb. Comput. Thierry Coquand, Henri Lombardi, Claude Quitté
2010	J	`jnl`	Games with 1-backtracking. Ann. Pure Appl. Log. Stefano Berardi, Thierry Coquand, Susumu Hayashi
2009	—	`conf`	A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA Andreas Abel, Thierry Coquand, Miguel Pagano
2009	B	`conf`	Forcing and Type Theory. CSL Thierry Coquand
2009	J	`jnl`	Integrals and valuations. J. Log. Anal. Thierry Coquand, Bas Spitters
2009	J	`jnl`	Space of valuations. Ann. Pure Appl. Log. Thierry Coquand
2009	J	`jnl`	Spectral schemes as ringed lattices. Ann. Math. Artif. Intell. Thierry Coquand, Henri Lombardi, Peter Schuster
2008	J	`jnl`	A note on the axiomatisation of real numbers. Math. Log. Q. Thierry Coquand, Henri Lombardi
2008	A	`conf`	Constructive Mathematics and Functional Programming (Abstract). ESOP Thierry Coquand
2008	Misc	`conf`	On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS Andreas Abel, Thierry Coquand, Peter Dybjer
2008	B	`conf`	Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC Andreas Abel, Thierry Coquand, Peter Dybjer
2007	J	`jnl`	A proof of strong normalisation using domain theory CoRR Thierry Coquand, Arnaud Spiwack
2007	J	`jnl`	A proof of strong normalisation using domain theory. Log. Methods Comput. Sci. Thierry Coquand, Arnaud Spiwack
2007	A*	`conf`	Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS Andreas Abel, Thierry Coquand, Peter Dybjer
2007	J	`jnl`	The Completeness of Typing for Context-Semantics. Fundam. Informaticae Thierry Coquand
2007	—	`conf`	Towards Constructive Homological Algebra in Type Theory. Calculemus/MKM Thierry Coquand, Arnaud Spiwack
2007	J	`jnl`	Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Informaticae Andreas Abel, Thierry Coquand
2006	A*	`conf`	A Proof of Strong Normalisation using Domain Theory. LICS Thierry Coquand, Arnaud Spiwack
2006	J	`jnl`	A logical approach to abstract algebra. Math. Struct. Comput. Sci. Thierry Coquand, Henri Lombardi
2006	—	`ch.`	Alfa/Agda. The Seventeen Provers of the World Thierry Coquand
2006	—	`ed.`	Mathematics, Algorithms, Proofs, 9.-14. January 2005 Mathematics, Algorithms, Proofs Thierry Coquand, Henri Lombardi, Marie-Françoise Roy
2006	J	`jnl`	Preface. Ann. Pure Appl. Log. Bernhard Banaschewski, Thierry Coquand, Giovanni Sambin
2006	J	`jnl`	Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. Gilles Barthe, Thierry Coquand
2005	—	`conf`	05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs Thierry Coquand, Henri Lombardi, Marie-Françoise Roy
2005	—	`conf`	05021 Executive Summary -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs Thierry Coquand
2005	C	`conf`	A Logical Approach to Abstract Algebra. CiE Thierry Coquand
2005	J	`jnl`	A Logical Framework with Dependently Typed Records. Fundam. Informaticae Thierry Coquand, Randy Pollack, Makoto Takeyama
2005	—	`conf`	A Nilregular Element Property. Mathematics, Algorithms, Proofs Thierry Coquand, Henri Lombardi, Peter Schuster
2005	J	`jnl`	A Short Proof for the Krull Dimension of a Polynomial Ring. Am. Math. Mon. Thierry Coquand, Henri Lombardi
2005	J	`jnl`	A constructive proof of the Peter-Weyl theorem. Math. Log. Q. Thierry Coquand, Bas Spitters
2005	—	`ch.`	An elementary characterisation of Krull dimension. From sets and types to topology and analysis Thierry Coquand, Henri Lombardi, Marie-Françoise Roy
2005	B	`conf`	Automating Coherent Logic. LPAR Marc Bezem, Thierry Coquand
2005	—	`conf`	Completeness Theorems and lambda-Calculus. TLCA Thierry Coquand
2005	—	`conf`	Connecting a Logical Framework to a First-Order Logic Prover. FroCoS Andreas Abel, Thierry Coquand, Ulf Norell
2005	J	`jnl`	Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. Univers. Comput. Sci. Thierry Coquand, Bas Spitters
2005	—	`conf`	Games with 1-backtracking. GALOP@ETAPS Stefano Berardi, Thierry Coquand, Susumu Hayashi
2005	—	`conf`	Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA Andreas Abel, Thierry Coquand
2004	—	`conf`	Formalising Bitonic Sort in Type Theory. TYPES Ana Bove, Thierry Coquand
2004	J	`jnl`	Proof-theoretical analysis of order relations. Arch. Math. Log. Sara Negri, Jan von Plato, Thierry Coquand
2003	—	`conf`	A Logical Framework with Dependently Typed Records. TLCA Thierry Coquand, Randy Pollack, Makoto Takeyama
2003	J	`jnl`	A representation of stably compact spaces, and patch topology. Theor. Comput. Sci. Thierry Coquand, Guo-Qiang Zhang
2003	J	`jnl`	A syntactical proof of the Marriage Lemma. Theor. Comput. Sci. Thierry Coquand
2003	B	`conf`	Dynamical Method in Algebra: A Survey. TABLEAUX Thierry Coquand
2003	J	`jnl`	Inductively generated formal topologies. Ann. Pure Appl. Log. Thierry Coquand, Giovanni Sambin, Jan M. Smith, Silvio Valentini
2003	J	`jnl`	Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. Bull. EATCS Marc Bezem, Thierry Coquand
2002	J	`jnl`	Metric Boolean algebras and constructive measure theory. Arch. Math. Log. Thierry Coquand, Erik Palmgren
2001	—	`conf`	A Finitary Subsystem of the Polymorphic lambda-Calculus. TLCA Thorsten Altenkirch, Thierry Coquand
2000	—	`conf`	An Implementation of Type: Type. TYPES Thierry Coquand, Makoto Takeyama
2000	—	`conf`	An Introduction to Dependent Type Theory. APPSEM Gilles Barthe, Thierry Coquand
2000	J	`jnl`	Formal Topologies on The Set of First-Order Formulae. J. Symb. Log. Thierry Coquand, Sara Sadocco, Giovanni Sambin, Jan M. Smith
2000	J	`jnl`	Intuitionistic choice and classical logic. Arch. Math. Log. Thierry Coquand, Erik Palmgren
2000	B	`conf`	Sequents, Frames, and Completeness. CSL Thierry Coquand, Guo-Qiang Zhang
2000	—	`ed.`	Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers TYPES Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith
1999	J	`jnl`	A Boolean Model of Ultrafilters. Ann. Pure Appl. Log. Thierry Coquand
1999	J	`jnl`	A new method for establishing conservativity of classical systems over their intuitionistic version. Math. Struct. Comput. Sci. Thierry Coquand, Martin Hofmann
1998	—	`conf`	A Note on Formal Iterated Function Systems. RealComp Thierry Coquand
1998	—	`conf`	Gröbner Bases in Type Theory. TYPES Thierry Coquand, Henrik Persson
1998	J	`jnl`	On the Computational Content of the Axiom of Choice. J. Symb. Log. Stefano Berardi, Marc Bezem, Thierry Coquand
1998	J	`jnl`	Two applications of Boolean models. Arch. Math. Log. Thierry Coquand
1997	B	`conf`	A Proof-Theoretical Investigation of Zantema's Problem. CSL Thierry Coquand, Henrik Persson
1997	J	`jnl`	Intuitionistic Model Constructions and Normalization Proofs. Math. Struct. Comput. Sci. Thierry Coquand, Peter Dybjer
1997	J	`jnl`	Minimal Invariant Spaces in Formal Topology. J. Symb. Log. Thierry Coquand
1996	J	`jnl`	An Algorithm for Type-Checking Dependent Types. Sci. Comput. Program. Thierry Coquand
1995	J	`jnl`	A Semantics of Evidence for Classical Arithmetic. J. Symb. Log. Thierry Coquand
1995	—	`conf`	A realization of the negative interpretation of the Axiom of Choice. TLCA Stefano Berardi, Marc Bezem, Thierry Coquand
1995	—	`conf`	An Application of Constructive Completeness. TYPES Thierry Coquand, Jan M. Smith
1995	B	`conf`	Program Construction in Intuitionistic Type Theory (Abstract). MPC Thierry Coquand
1994	J	`jnl`	A - Translation and Looping Combinators in Pure Type Systems. J. Funct. Program. Thierry Coquand, Hugo Herbelin
1994	J	`jnl`	An Analysis of Ramsey's Theorem Inf. Comput. Thierry Coquand
1994	—	`conf`	Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS Thierry Coquand, Peter Dybjer
1994	J	`jnl`	Type Theorie Programming. Bull. EATCS Thierry Coquand, Bengt Nordström, Jan M. Smith, Björn von Sydow
1993	J	`jnl`	Another Proof of the Intuitionistic Ramsey Theorem. Theor. Comput. Sci. Thierry Coquand
1993	—	`conf`	Infinite Objects in Type Theory. TYPES Thierry Coquand
1992	J	`jnl`	An Intuitionistic Proof of Tychonoff's Theorem. J. Symb. Log. Thierry Coquand
1992	J	`jnl`	The Paradox of Trees in Type Theory. BIT Thierry Coquand
1991	—	`conf`	A Direct Proof of the Intuitionistic Ramsey Theorem. Category Theory and Computer Science Thierry Coquand
1991	—	`conf`	Constructive Topology and Combinatorics. Constructivity in Computer Science Thierry Coquand
1991	J	`jnl`	Inheritance as Implicit Coercion Inf. Comput. Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov
1989	J	`jnl`	Categories of Embeddings. Theor. Comput. Sci. Thierry Coquand
1989	J	`jnl`	Domain Theoretic Models of Polymorphism Inf. Comput. Thierry Coquand, Carl A. Gunter, Glynn Winskel
1989	A*	`conf`	Inheritance and Explicit Coercion (Preliminary Report) LICS Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov
1988	A*	`conf`	Categories of Embeddings LICS Thierry Coquand
1988	J	`jnl`	Extensional Models for Polymorphism. Theor. Comput. Sci. Val Tannen, Thierry Coquand
1988	—	`conf`	Inductively defined types. Conference on Computer Logic Thierry Coquand, Christine Paulin
1988	J	`jnl`	The Calculus of Constructions Inf. Comput. Thierry Coquand, Gérard P. Huet
1987	—	`conf`	An Equational Presentation of Higher Order Logic. Category Theory and Computer Science Thierry Coquand, Thomas Ehrhard
1987	B	`conf`	DI-Domains as a Model of Polymorphism. MFPS Thierry Coquand, Carl A. Gunter, Glynn Winskel
1987	—	`conf`	Extensional Models for Polymorphism. TAPSOFT, Vol.2 Val Tannen, Thierry Coquand
1986	A*	`conf`	An Analysis of Girard's Paradox LICS Thierry Coquand
1985	J	`jnl`	A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. J. Symb. Comput. Thierry Coquand, Gérard P. Huet
1985	—	`conf`	Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Logic Colloquium Thierry Coquand, Gérard P. Huet
1985	—	`conf`	Constructions: A Higher Order Proof System for Mechanizing Mathematics. European Conference on Computer Algebra (1) Thierry Coquand, Gérard P. Huet
1985	—	`conf`	Sur l'Analogie entre les Propositions et les Types. Combinators and Functional Programming Languages Thierry Coquand