Lars Birkedal – An Introduction to Iris: Higher-Order Concurrent Separation Logic

September 23rd, 2021 – 11:00 am

Modern programming languages such as Java, Scala, and Rust are examples of concurrent higher-order imperative programming languages.

In this talk I will give an introduction to our research on Iris, a logical framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs.


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, the recipient of a Villum Investigator grant from the Villum Foundation 2019, the Danish Minister of Research Elite Research Award 2015 (« Videnskabsministeriets EliteForsk-pris »), and the ACM SIGPLAN Milner Award 2013.

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 concurrent, higher-order, and imperative programs; cyber-security; and type theories with guarded recursion.

The presentation will be in English and will be held at Inria Sophia Antipolis, amphi Kahn.

Physical* or virtual attendance. Please register via this link or directly below.

If you encounter problems registering online, please send an email to confirming you physical ou virtual attendance.

*Physical presence: sanitary pass will be required for all partipants (Inria or non Inria) and organizers

Les organisateurs et les agents Inria présents lors de l’événement sont également soumis à l’obligation du pass sanitaire

Les commentaires sont clos.