Unifying Speaker Lars Birkedal
Lars Birkedal is Professor of Computer Science at Aarhus University. He received his Ph.D. in Computer Science from Carnegie Mellon University, USA, in Dec. 1999 and until Dec. 2012 he was at the IT University of Copenhagen, Denmark. He served as Head of Department of Computer Science in Aarhus from 2014 to 2017. Lars Birkedal is a Fellow of the ACM, an elected member of the Royal Danish Academy of Sciences and Letters, recipient of an ERC Advanced Grant from the European Research Council 2023, the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation (for the design and implementation of Iris, a higher-order concurrent separation logic framework), a Villum Investigator grant from the Villum Foundation 2019, the Danish Minister of Research Elite Research Award 2015 (Videnskabsministeriets EliteForsk-pris), a Sapere Aude Advanced Grant from the Danish National Science Research Council 2013, and the ACM SIGPLAN Milner Award 2013. He served as the Editor-in-Chief of the journal Logical Methods in Computer Science from 2014 until 2020 and is now Chairman of the board of the journal, and served as PC Chair for the POPL 2020 conference. Lars Birkedal’s main research interests lie in the area of logic and semantics of programming languages and type theories. Current work focuses on program logics for reasoning about distributed, concurrent, higher-order, and imperative programs; cyber-security; and type theories with guarded recursion.
Talk
Higher-Order Probabilistic Relational Separation Logic
Monday, 9:00
Room: Europe A
In the last 10–15 years, we have seen how higher-order separation logic is very effective for formal modular reasoning about full functional correctness of higher-order imperative programs. Moreover, relational higher-order separation logics have proved useful for reasoning about relational properties such as contextual refinement and noninterference, and several such relational separation logics have been formalized on top of the Iris framework in Coq.
In this talk I will present some of our recent work on extending relational higher-order separation logic to probabilistic higher-order imperative programming languages, and show how two new probabilistic relational higher-order separation logics, called Clutch and Caliper, can be used to reason about contextual refinement and almost sure termination of probabilistic higher-order imperative programs. In particular, I will emphasize how we can leverage separation-logic-style reasoning to obtain novel reasoning principles and verify examples beyond earlier probabilistic program logics.
All results have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.
The talk is based on joint work with Simon Gregersen, Alejandro Aguirre, Philipp Haselwater, Joseph Tassarotti, Kwing Hei-Li, and Markus de Medeiros, some of which has been published in the following paper:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
S.O. Gregersen, A. Aguirre, P.G. Haselwarter, J. Tassarotti, and L. Birkedal.
In Proceedings of POPL 2024.