POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Fri 24 Jan 2025 14:00 - 14:20 at Peek-A-Boo - Program Logics 2

We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers à la Dijkstra and through the lens of Kleene algebra with top and tests (TopKAT). Our main goal is to give an overview – a taxonomy – of how these program logics relate, in particular under different assumptions like for example program termination, determinism, and reversibility. As a byproduct, we obtain a TopKAT characterization of Lisbon logic, which – to the best of our knowledge – is a novel result.

This program is tentative and subject to change.

Fri 24 Jan

Displayed time zone: Mountain Time (US & Canada) change

13:20 - 14:20
Program Logics 2POPL at Peek-A-Boo
13:20
20m
Talk
BiSikkel: A Multimode Logical Framework in Agda
POPL
Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
13:40
20m
Talk
Calculational Design of Hyperlogics by Abstract Interpretation
POPL
Patrick Cousot , Jeffery Wang CIMS, New York University
14:00
20m
Talk
A Taxonomy of Hoare-Like Logics
POPL
Lena Verscht RWTH Aachen University; Saarland University, Benjamin Lucien Kaminski Saarland University; University College London