Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                            Salle A215, bâtiment A
                          Mercredi 7 décembre, 10h30

                               Yannick Forster
                                    Inria

                Towards Verified Extraction from Coq to OCaml

A central claim to fame of the Coq proof assistant is extraction to
languages like OCaml, centrally used in landmark projects such as
CompCert. Extraction was initially conceived and implemented by Pierre
Letouzey, and is still guiding design decisions of Coq's type theory.
While the core extraction algorithm is verified on paper, central
features like optimisations -- of which there are 10 the user can
enable -- only have empirical correctness guarantees.

In the scope of the MetaCoq project, which aims at placing Coq's type
theory on a well-defined and fully formal foundation, I am working
with other members of the MetaCoq team on a re-implementation and
verification of all aspects of Coq's extraction process to OCaml. The
new extraction process is based on a formal semantics of Coq as
provided by MetaCoq and a formal semantics of the intermediate
language of the OCaml compiler as provided by the Malfunction project.

In my talk, I plan on discussing the current state of this
verification, its goals, possible extensions, and design decisions
along the way, a discussion of the trusted computing and theory bases
(and in particular ideas for reducing them), arising problems with Coq
and the surrounding infrastructure, impact on other projects, and
thoughts on maintainability, modularity, and accessibility of proofs.

            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