Hazel: a Separation Logic for effect handlers

Speaker: Paulo de Vilhena, Inria Paris.
Tuesday 19 April 2022, 11:00, (room 1Z31 ENS Paris-Saclay and online)

Abstract: 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.