36 citations · 143 across the 40 of their papers we have counts for
Showing 2026Show all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2026
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…
cs.LO2026
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…