Thierry Coquand

Orcid: 0000-0002-5429-5153

Affiliations:
  • University of Gothenburg, Sweden


According to our database1, Thierry Coquand authored at least 141 papers between 1985 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
The equivariant model structure on cartesian cubical sets.
CoRR, 2024

A Variation of Reynolds-Hurkens Paradox.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024

Some Remarks About Dependent Type Theory.
Proceedings of the French School of Programming, 2024

2023
Reduction Free Normalisation for a proof irrelevant type of propositions.
Log. Methods Comput. Sci., 2023

2022
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism.
Theor. Comput. Sci., 2022

Canonicity and homotopy canonicity for cubical type theory.
Log. Methods Comput. Sci., 2022

Type Theories with Universe Level Judgements.
CoRR, 2022

Controlling unfolding in type theory.
CoRR, 2022

Type Theory with Explicit Universe Polymorphism.
Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021
Constructive sheaf models of type theory.
Math. Struct. Comput. Sci., 2021

On generalized algebraic theories and categories with families.
Math. Struct. Comput. Sci., 2021

Syntax and models of Cartesian cubical type theory.
Math. Struct. Comput. Sci., 2021

Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472).
Dagstuhl Reports, 2021

2020
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality.
Log. Methods Comput. Sci., 2020

A Note on Generalized Algebraic Theories and Categories with Families.
CoRR, 2020

2019
Canonicity and normalization for dependent type theory.
Theor. Comput. Sci., 2019

An Adequacy Theorem for Dependent Type Theory.
Theory Comput. Syst., 2019

Preface to the special issue for The Fifth Workshop on Formal Topology.
J. Log. Anal., 2019

The Univalence Axiom in Cubical Sets.
J. Autom. Reason., 2019

Skolem's Theorem in Coherent Logic.
Fundam. Informaticae, 2019

Homotopy Canonicity for Cubical Type Theory.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018
A survey of constructive presheaf models of univalence.
ACM SIGLOG News, 2018

Canonicity and normalisation for Dependent Type Theory.
CoRR, 2018

On Higher Inductive Types in Cubical Type Theory.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Inner Models of Univalence.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017
The Independence of Markov's Principle in Type Theory.
Log. Methods Comput. Sci., 2017

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.
FLAP, 2017

Notions of Anonymous Existence in Martin-Löf Type Theory.
Log. Methods Comput. Sci., 2017

Stack semantics of type theory.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Type Theory and Formalisation of Mathematics.
Proceedings of the Computer Science - Theory and Applications, 2017

2016
A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic.
CoRR, 2016

Preface.
Ann. Pure Appl. Log., 2016

Realizability at Work: Separating Two Constructive Notions of Finiteness.
Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic.
Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

The Ackermann Award 2016.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015
A Kripke model for simplicial sets.
Theor. Comput. Sci., 2015

A generalization of the Takeuti-Gandy interpretation.
Math. Struct. Comput. Sci., 2015

A Presheaf Model of Parametric Type Theory.
Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

Non-Constructivity in Kan Simplicial Sets.
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014
A Sheaf Model of the Algebraic Closure.
Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

2013
Computing persistent homology within Coq/SSReflect.
ACM Trans. Comput. Log., 2013

Dynamic Newton-Puiseux theorem.
J. Log. Anal., 2013

About Goodman's Theorem.
Ann. Pure Appl. Log., 2013

A Model of Type Theory in Cubical Sets.
Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Generalizations of Hedberg's Theorem.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2012
A Computational Interpretation of Forcing in Type Theory.
Proceedings of the Epistemology versus Ontology, 2012

A constructive proof of Simpson's Rule.
J. Log. Anal., 2012

A formal proof of Sasaki-Murao algorithm.
J. Formaliz. Reason., 2012

Preface.
Ann. Pure Appl. Log., 2012

Stop When You Are Almost-Full - Adventures in Constructive Termination.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

The Ackermann Award 2012.
Proceedings of the Computer Science Logic (CSL'12), 2012

Coherent and Strongly Discrete Rings in Type Theory.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Metric complements of overt closed sets.
Math. Log. Q., 2011

Unique paths as formal points.
J. Log. Anal., 2011

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Log. Methods Comput. Sci., 2011

A Decision Procedure for Regular Expression Equivalence in Type Theory.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
Curves and coherent Prüfer rings.
J. Symb. Comput., 2010

Constructive theory of Banach algebras.
J. Log. Anal., 2010

A Note on Forcing and Type Theory.
Fundam. Informaticae, 2010

Games with 1-backtracking.
Ann. Pure Appl. Log., 2010

2009
Integrals and valuations.
J. Log. Anal., 2009

Space of valuations.
Ann. Pure Appl. Log., 2009

Spectral schemes as ringed lattices.
Ann. Math. Artif. Intell., 2009

Forcing and Type Theory.
Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008
A note on the axiomatisation of real numbers.
Math. Log. Q., 2008

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.
Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.
Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Constructive Mathematics and Functional Programming (Abstract).
Proceedings of the Programming Languages and Systems, 2008

2007
A proof of strong normalisation using domain theory.
Log. Methods Comput. Sci., 2007

The Completeness of Typing for Context-Semantics.
Fundam. Informaticae, 2007

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
Fundam. Informaticae, 2007

Towards Constructive Homological Algebra in Type Theory.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006
A logical approach to abstract algebra.
Math. Struct. Comput. Sci., 2006

Remarks on the equational theory of non-normalizing pure type systems.
J. Funct. Program., 2006

Preface.
Ann. Pure Appl. Log., 2006

Alfa/Agda.
Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005
A Short Proof for the Krull Dimension of a Polynomial Ring.
Am. Math. Mon., 2005

A constructive proof of the Peter-Weyl theorem.
Math. Log. Q., 2005

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems.
J. Univers. Comput. Sci., 2005

A Logical Framework with Dependently Typed Records.
Fundam. Informaticae, 2005

Completeness Theorems and lambda-Calculus.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Automating Coherent Logic.
Proceedings of the Logic for Programming, 2005

Connecting a Logical Framework to a First-Order Logic Prover.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

A Nilregular Element Property.
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

05021 Abstracts Collection -- Mathematics, Algorithms, Proofs.
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

05021 Executive Summary -- Mathematics, Algorithms, Proofs.
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

A Logical Approach to Abstract Algebra.
Proceedings of the New Computational Paradigms, 2005

An elementary characterisation of Krull dimension.
Proceedings of the From sets and types to topology and analysis, 2005

2004
Proof-theoretical analysis of order relations.
Arch. Math. Log., 2004

Formalising Bitonic Sort in Type Theory.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2003
A representation of stably compact spaces, and patch topology.
Theor. Comput. Sci., 2003

A syntactical proof of the Marriage Lemma.
Theor. Comput. Sci., 2003

Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column.
Bull. EATCS, 2003

Inductively generated formal topologies.
Ann. Pure Appl. Log., 2003

Dynamical Method in Algebra: A Survey.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003

2002
Metric Boolean algebras and constructive measure theory.
Arch. Math. Log., 2002

2001
A Finitary Subsystem of the Polymorphic lambda-Calculus.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

2000
Formal Topologies on The Set of First-Order Formulae.
J. Symb. Log., 2000

Intuitionistic choice and classical logic.
Arch. Math. Log., 2000

An Implementation of Type: Type.
Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Sequents, Frames, and Completeness.
Proceedings of the Computer Science Logic, 2000

An Introduction to Dependent Type Theory.
Proceedings of the Applied Semantics, International Summer School, 2000

1999
A new method for establishing conservativity of classical systems over their intuitionistic version.
Math. Struct. Comput. Sci., 1999

A Boolean Model of Ultrafilters.
Ann. Pure Appl. Log., 1999

1998
On the Computational Content of the Axiom of Choice.
J. Symb. Log., 1998

A Note on Formal Iterated Function Systems.
Proceedings of the Workshop on Real Number Computation, 1998

Two applications of Boolean models.
Arch. Math. Log., 1998

Gröbner Bases in Type Theory.
Proceedings of the Types for Proofs and Programs, 1998

1997
Intuitionistic Model Constructions and Normalization Proofs.
Math. Struct. Comput. Sci., 1997

Minimal Invariant Spaces in Formal Topology.
J. Symb. Log., 1997

A Proof-Theoretical Investigation of Zantema's Problem.
Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996
An Algorithm for Type-Checking Dependent Types.
Sci. Comput. Program., 1996

1995
A Semantics of Evidence for Classical Arithmetic.
J. Symb. Log., 1995

An Application of Constructive Completeness.
Proceedings of the Types for Proofs and Programs, 1995

A realization of the negative interpretation of the Axiom of Choice.
Proceedings of the Typed Lambda Calculi and Applications, 1995

Program Construction in Intuitionistic Type Theory (Abstract).
Proceedings of the Mathematics of Program Construction, 1995

1994
An Analysis of Ramsey's Theorem
Inf. Comput., May, 1994

A - Translation and Looping Combinators in Pure Type Systems.
J. Funct. Program., 1994

Type Theorie Programming.
Bull. EATCS, 1994

Inductive Definitions and Type Theory: an Introduction (Preliminary Version).
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1993
Another Proof of the Intuitionistic Ramsey Theorem.
Theor. Comput. Sci., 1993

Infinite Objects in Type Theory.
Proceedings of the Types for Proofs and Programs, 1993

1992
An Intuitionistic Proof of Tychonoff's Theorem.
J. Symb. Log., 1992

The Paradox of Trees in Type Theory.
BIT, 1992

1991
Inheritance as Implicit Coercion
Inf. Comput., July, 1991

A Direct Proof of the Intuitionistic Ramsey Theorem.
Proceedings of the Category Theory and Computer Science, 1991

Constructive Topology and Combinatorics.
Proceedings of the Constructivity in Computer Science, 1991

1989
Domain Theoretic Models of Polymorphism
Inf. Comput., May, 1989

Categories of Embeddings.
Theor. Comput. Sci., 1989

Inheritance and Explicit Coercion (Preliminary Report)
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1988
Extensional Models for Polymorphism.
Theor. Comput. Sci., 1988

The Calculus of Constructions
Inf. Comput., 1988

Inductively defined types.
Proceedings of the COLOG-88, 1988

1987
DI-Domains as a Model of Polymorphism.
Proceedings of the Mathematical Foundations of Programming Language Semantics, 1987

An Equational Presentation of Higher Order Logic.
Proceedings of the Category Theory and Computer Science, 1987

1986
An Analysis of Girard's Paradox
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

1985
A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction.
J. Symb. Comput., 1985

Concepts mathématiques et informatiques formalisés dans le calcul des constructions.
Proceedings of the Logic Colloquium '85, Orsay, France, 1985

Sur l'Analogie entre les Propositions et les Types.
Proceedings of the Combinators and Functional Programming Languages, 1985

Constructions: A Higher Order Proof System for Mechanizing Mathematics.
Proceedings of the EUROCAL '85, 1985


  Loading...