Write a Blog >>
Thu 23 Jan 2020 15:56 - 16:18 at Ile de France II (IDF II) - Program Logics Chair(s): Chung-Kil Hur

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic characterization for relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that by instantiating our framework with state and unbounded iteration we can reconstruct a variant of Benton’s Relational Hoare Logic. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with effects such as exceptions, and are the first to provide a proper semantic foundation and a relational program logic for exceptions.

Slides of the presentation (TheNext700RelationalProgramLogics.pdf)849KiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 16:40
Program LogicsResearch Papers at Ile de France II (IDF II)
Chair(s): Chung-Kil Hur Seoul National University
15:35
21m
Talk
Deductive Verification with Ghost Monitors
Research Papers
Martin Clochard ETH Zürich, Claude Marché Inria Saclay & Université Paris-Saclay, Andrei Paskevich LRI, Université Paris-Sud & CNRS
Link to publication DOI Media Attached
15:56
21m
Talk
The Next 700 Relational Program Logics
Research Papers
Kenji Maillard Inria Nantes & University of Chile, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Antoine Van Muylder Inria Paris and Paris 7
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Incorrectness Logic
Research Papers
Peter O'Hearn Facebook
Link to publication DOI Media Attached