Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                            Salle A215, bâtiment A
                         Vendredi 17 novembre, 10h30

                                Samuel Vivien
                                 Inria Paris

                       How to prove that you need Cake?

PureCake is a mechanically-verified compiler for PureLang, a lazy,
purely functional programming language. This compiler has been
developed on top of the CakeML compiler as part of the CakeML project.
This talk will present a global overview of the compiler and focus on
how the compiler was verified and on the demand analysis pass.

The talk is based on the paper "PureCake: A Verified Compiler for a
Lazy Functional Language" [PLDI'23] by Hrutvik Kanabar, Samuel Vivien,
Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman
Pohjola, Riccardo Zanetti.

            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.