We give a formalised and machine-checked account of computability theory in the Calculus
of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof …

We formalise the undecidability of solvability of Diophantine equations, ie polynomial
equations over natural numbers, in Coq's constructive type theory. To do so, we give the first …

In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops
computability theory without an explicit model of computation. This is enabled by assuming …

We present a framework for the verified programming of multi-tape Turing machines in Coq.
Improving on prior work by Asperti and Ricciotti in Matita, we implement multiple layers of …

Abstract We mechanise the Cook-Levin theorem, ie the NP-completeness of SAT, in the
proof assistant Coq. We use the call-by-value λ-calculus L as the model of computation to …

We formalise undecidability results concerning higher-order unification in the simply-typed λ-
calculus with β-conversion in Coq. We prove the undecidability of general higher-order …

Reversible primitive permutations (RPP) is a class of recursive functions that models
reversible computation. We present a proof, which has been verified using the proof …

In this thesis, we investigate several key results in the canon of metamathematics, applying
the contemporary perspective of formalisation in constructive type theory and mechanisation …

Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and
is used in the fields of Artificial Intelligence, cryptography, and coding theory. The …

We present a generalised, constructive, and machine-checked approach to Kolmogorov
complexity in the constructive type theory underlying the Coq proof assistant. By proving that …