Séminaire Cambium, Inria Paris
                                 Amphi Lions
                          Mercredi 9 octobre, 10h30

                                 Pedro Abreu
                              Purdue University

                   A Translation of GADTs in OCaml into Coq

Proof assistants based on dependent types are powerful tools for building
certified software. In order to verify programs written in a different
language, however, a representation of those programs in the proof
assistant is required. One challenge with this approach is ensuring that
any semantic gaps between the two languages are accounted for.

This work introduces GSet, a mixed embedding that bridges the gap between
OCaml GADTs and inductive datatypes in Coq. This embedding retains the
rich typing information of GADTs while also allowing pattern matching with
impossible branches to be translated without additional axioms. For this,
we develop two minimal calculus that captures the essence of our
translation algorithm: GADTml and gCIC, and we prove its soundness. We
have integrated this technique into coq-of-ocaml, a tool for automatically
translating OCaml programs into Coq. Finally, we demonstrate the
feasibility of our approach by using our enhanced version of coq-of-ocaml,
to translate a portion of the Tezos code base into Coq.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.