Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic

Robbert Krebbers

Date: Wed, February 07, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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 talk I will give an introduction to Iris and its implementation in Coq.

Previous: Albert ten Napel |
Next: Wiebe van Geest |