LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
Formalisation and Meta-Theory of Type Theory
- Date
- 12.01.2021, 11:00
- Place
- online
- Speaker
- Theo Winterhalter (MPI for Security and Privacy)
In this talk I will present part of the work I did during my PhD thesis. I worked on the meta-theory of type theory and its formalisation in a proof assistant. I will mainly show my work for the MetaCoq project which consists in 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 and complete 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---strong normalisation---have to be assumed, i.e. taken as axioms. I will also briefly talk about how this allowed me to formalise an extension of Coq with rewrite rules.