From the 1 of 10 linked papers with an AI index.
10 papers
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
The paper presents a domain‑theoretic proof technique that establishes definitional inversion properties (injectivity and no‑confusion) of type constructors in dependent type syste…
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…
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, foll…
Azumaya algebras and Barr Theorem
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivale…
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…
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ématiqu…