36 citations · 143 across the 40 of their papers we have counts for
17 papers · 1 filter
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity a…
Auto formalisation of Chaitin and of the surprise incompleteness Theorem
Thierry Coquand
This is a continuation of a previous report on an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. Using the framework built in this e…
Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
Thierry Coquand
We report an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. The theorem is formalised for Church's Basic Recursive Arithmetic, follo…
A variation of Reynolds-Hurkens Paradox
Thierry Coquand
We present a variation of Hurkens paradox, which can itself be seen as a variation of Reynolds result that there is no set theoretic model of polymorphism.
Type Theory with Explicit Universe Polymorphism (revised and extended version)
Marc Bezem, Thierry Coquand, Peter Dybjer +1
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on e…
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
Reduction Free Normalisation for a proof irrelevant type of propositions
Thierry Coquand
We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used…
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Andreas Abel, Thierry Coquand
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from…
On Higher Inductive Types in Cubical Type Theory
Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles…
Stack Semantics of Type Theory
Thierry Coquand, Bassel Mannaa, Fabian Ruch
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As…
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber +1
This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent…
Notions of Anonymous Existence in Martin-Löf Type Theory
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
Robin Adams, Marc Bezem, Thierry Coquand
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property o…
The Independence of Markov's Principle in Type Theory
Thierry Coquand, Bassel Mannaa
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov…
Computing Persistent Homology within Coq/SSReflect
Jónathan Heras, Thierry Coquand, Anders Mörtberg +1
Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis o…
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Andreas Abel, Thierry Coquand, Miguel Pagano
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluati…
A proof of strong normalisation using domain theory
Thierry Coquand, Arnaud Spiwack
Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recu…