Séminaire Cambium, Inria Paris
                                     BJ09
                           Lundi 25 novembre, 14h00

                               Yannick Zakowski
                                  Inria Lyon

      Abstract Interpreters: A Monadic Approach to Modular Verification

In this talk, I shall start by putting in context a series of work
exploring in a broad sense a methodology based on shallow representations
of computations in Coq. I will then more specifically focus on a recent
piece of work that argues that such monadic interpreters built as layers
of interpretations stacked atop the free monad constitute a promising way
to implement and verify abstract interpreters.

The approach enables modular proofs of soundness of the resulting
interpreters. We provide generic abstract control flow combinators proven
correct once and for all against their concrete counterpart. We
demonstrate how to relate concrete handlers implementing effects to
abstract variants of these handlers, essentially capturing the traditional
soundness of transfer functions in the context of monadic interpreters.
Finally, we provide generic results to lift soundness statements via the
interpretation of stateful and failure effects.

We have formalized all the aforementioned combinators and theories in Coq,
and demonstrated their benefits by implementing and proving correct two
illustrative abstract interpreters for a structured imperative language
and a toy assembly.

This contribution is joint work with Sébastien Michelland and Laure
Gonnord, and has been the focus of a paper at ICFP'24.

            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.