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) Salle Lions 1, bâtiment C Lundi 29 novembre, 10h30 ----------------------- Paulo Emílio de Vilhena ----------------------- Inria Paris ============================================= Hazel: a Separation Logic for effect handlers ============================================= A program logic is a pair of a language, for writing specifications, and a set of reasoning rules, for deriving specifications. In this talk, I present Hazel, a program logic for effect handlers. I start by laying out the motivation for such work and then I present its main ideas: how to write the specification of effectful programs in Hazel and what reasoning principles does it suggest? Finally, I apply these ideas to `invert`, a function that exploits effect handlers to produce a lazy sequence (a cascade) out of a higher-order iteration function.