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 25 janvier, 15h00

                             -------------------
                             Clément Pit-Claudel
                             -------------------


         ===========================================================
            Extensible Extraction of Efficient Imperative Programs
         with Foreign Functions, Manually Managed Memory, and Proofs
         ===========================================================

We present an original approach to sound program extraction in a proof
assistant, using syntax-driven automation to derive correct-by-construction
imperative programs from nondeterministic functional source code. Our approach
does not require committing to a single inflexible compilation strategy and
instead makes it straightforward to create domain-specific code translators.
In addition to a small set of core definitions, our framework is a large,
user-extensible collection of compilation rules each phrased to handle
specific language constructs, code patterns, or data manipulations. By mixing
and matching these pieces of logic, users can easily tailor extraction to
their own domains and programs, getting maximum performance and ensuring
correctness of the resulting assembly code. Using this approach, we complete
the first proof-generating pipeline that goes automatically from high-level
specifications to assembly code. In our main case study, the original
specifications are phrased to resemble SQL-style queries, while the final
assembly code does manual memory management, calls out to foreign data
structures and functions, and is suitable to deploy on resource-constrained
platforms. The pipeline runs entirely within the Coq proof assistant, leading
to final, linked assembly code with overall full-functional-correctness proofs
in separation logic.

This is joint work with Peng Wang, Benjamin Delaware, Jason Gross, and Adam
Chlipala.