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 object capabilities, 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.

Mon 8 Jan

POPL-2018-TutorialFest
14:00 - 15:30: TutorialFest - Iris - A Higher-Order Concurrent Separation Logic at Museum B
POPL-2018-TutorialFest151541640000014:00 - 15:30
Talk
Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology
Media Attached
POPL-2018-TutorialFest
16:00 - 17:00: TutorialFest - Iris - A Higher-Order Concurrent Separation Logic at Museum B
POPL-2018-TutorialFest151542360000016:00 - 17:00
Talk
Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology
Media Attached