Vous pouvez vous abonner à nos annonces de séminaires:
http://cambium.inria.fr/seminar.html
Nos séminaires sont accessibles en ligne en direct:
https://webconf.math.cnrs.fr/b/fra-ryy-fjn
S É M I N A I R E
______ __ _
/ ____/___ _____ ___ / /_ (_)_ ______ ___
/ / / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
/ /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
\____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/
I N R I A - Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
En ligne
Lundi 1 février, 10h30
-----------------
Théo Winterhalter
-----------------
Inria
=========================================================
Coq Coq Correct!
Verification of Type Checking and Erasure for Coq, in Coq
=========================================================
Coq is built around a well-delimited kernel that perfoms typechecking for
definitions in a variant of the Calculus of Inductive Constructions
(CIC). Although the metatheory of CIC is very stable and reliable, the
correctness of its implementation in Coq is less clear. Indeed, implementing
an efficient type checker for CIC is a rather complex task, and many parts of
the code rely on implicit invariants which can easily be broken by further
evolution of the code. Therefore, on average, one critical bug has been found
every year in Coq.
This paper presents the first implementation of a type checker for the kernel
of Coq (without the module system and template polymorphism), which is proven
correct and complete in Coq with respect to its formal specification and
axiomatisation of part of its metatheory. Note that because of Gödel’s
incompleteness theorem, there is no hope to prove completely the correctness
of the specification of Coq inside Coq (in particular strong normalisation or
canonicity), but it is possible to prove the correctness of the implementation
assuming the correctness of the specification, thus moving from a trusted code
base (TCB) to a trusted theory base (TTB) paradigm.
Our work is based on the MetaCoq project which provides metaprogramming
facilities to work with terms and declarations at the level of this
kernel. Our type checker is based on the specification of the typing relation
of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at
the basis of Coq and the verification of a relatively efficient and sound
type-checker for it. In addition to the kernel implementation, an essential
feature of Coq is the so-called extraction: the production of executable code
in functional languages from Coq definitions. We present a verified version of
this subtle type-and-proof erasure step, therefore enabling the verified
extraction of a safe type-checker for Coq.