36 citations · 143 across the 40 of their papers we have counts for
45 papers
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…
In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl
Stefan Neuwirth, Henri Lombardi, Thierry Coquand
In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the tradi…
Heitmann dimension of distributive lattices and commutative rings
Thierry Coquand, Henri Lombardi, Claude Quitté
This paper is the English translation of the first 4 sections of the article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématique…
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.