The Coq mailing list

[Théo Winterhalter <theo.winterhalter AT csp.mpg.de>]

To anyone interested I am pleased to announce that I successfully defended my PhD thesis called « Formalisation and Meta-Theory of Type Theory » and that the manuscript as well as the recording of my defence are freely available online:

Manuscript: https://github.com/TheoWinterhalter/phd-thesis/releases/tag/v1.2.1

Defence video: https://www.youtube.com/watch?v=sEr7sz1sOAk

I defended it in front (mostly virtually) of the following jury:

President: Gilles DOWEK

Reviewers: 

Andrej BAUER

Herman GEUVERS

Jury:

Andreas ABEL

Hugo HERBELIN

Assia MAHBOUBI

Bas SPITTERS

Advisors:

Nicolas TABAREAU

Matthieu SOZEAU

Abstract:

In this thesis, I talk about the meta-theory of type theory and about how to formalise it in a proof assistant.

I first focus on a conservative translation between extensional type theory and either intensional or weak type theory, entirely written in Coq. The first translation consists in a removal of the reflection of equality rule, whereas the second translation produces something stronger: weak type theory is a type theory with no notion of conversion. The conservativity result implies that conversion doesn't increase the logical power of type theories.

Then, I show my work for the MetaCoq project of formalising and specifying Coq within Coq. In particular I worked on writing a type-checker for Coq, in Coq. This type checker is proven sound with respect to the specification and can be extracted to OCaml code and run independently of Coq's kernel type-checker. For this to work we have to rely on the meta-theory of Coq which we develop, in part, in the MetaCoq project. However, because of Gödel's incompleteness theorems, we cannot prove consistency of Coq within Coq, and this means that some properties---mainly strong normalisation---have to be assumed, i.e. taken as axioms.