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

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.