Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E ______ __ _ / ____/___ _____ ___ / /_ (_)_ ______ ___ / / / __ `/ __ `__ \/ __ \/ / / / / __ `__ \ / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / / \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 17 février, 10h30 ------------ Thomas Letan ------------ ANSSI/SDE/DST/LSL ============================================================= Implementing and Certifying Impure Computations with FreeSpec ============================================================= In this talk, we present FreeSpec, a framework for the Coq theorem prover which we use to implement (using a Free monad) and certify (using contracts) impure computations. FreeSpec has notably been used to implement a clone of `ar', and a minimal HTTP server. We first give an overview of FreeSpec formalism, with a focus on how it allows compositional reasoning, similar to how monads allow for compositional implementations. Then, we present FreeSpec proof-engineering approach and tools. Our ambition is to make programming impure (certified!) computations in Coq as straightforward as in other functional programming languages. Finally, we discuss future work, in particular our project to provide a pleasant POSIX package for Coq.