Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:00 - 19:30 at TutorialFest-B - Tutorial 5

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for fault-tolerant systems code, and a safety proof for a realistic subset of the Rust programming language.

In this tutorial, you will learn how use the Iris framework to reason about concurrent programs. This tutorial will be hands-on: we will use the Coq implementation of Iris to mechanize our proofs. It is recommended to come with Coq and Iris pre-installed on your machine so that you can play with Iris yourself. You can follow the installation instructions in the tutorial exercises git repository.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 19:30
[T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic
Tej ChajedMassachusetts Institute of Technology, USA, Ralf JungMPI-SWS, Joseph TassarottiBoston College
Link to publication