36 citations · 55 across the 13 of their papers we have counts for
6 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.
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…
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…