Hazel: a Separation Logic for effect handlers

Apr 19 11:00 ₂₀₂₂

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.