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

Displayed 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 Chajed Massachusetts Institute of Technology, USA, Ralf Jung MPI-SWS, Joseph Tassarotti Boston College
Link to publication