Séminaire Cambium, Inria Paris
                            Room to be determined
                         Vendredi 13 septembre, 10h30

                               Jacques Garrigue
                              Nagoya University

          Mechanized monadic equational reasoning for ML references

We extend a Coq formalization of monadic equational reasoning with a
monad to represent typed stores. This leads us to design an original
equational theory, that we experimented on a number of examples. The
examples themselves are generated from OCaml programs using an
experimental compiler from OCaml to Coq, which targets the typed store
monad.

This is joint work with Reynald Affeldt (AIST) and Masafumi Saikawa
(Nagoya U).

            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.