POPL 2017
Sun 15 - Sat 21 January 2017
Sun 15 Jan 2017 16:00 - 16:50 at Salle 105, Barre 44-54 - Second Afternoon Session Chair(s): Hugo Herbelin

In this talk I will give an overview of the Iris project. Firstly, I will present the Iris base logic, which is a small resourceful logic that can be used to develop complex separation logics in a layered way. This base logic only comprises the assertion layer of vanilla separation logic, plus a handful of simple modalities. The much fancier logical mechanisms of the Iris program logic, such as Hoare triples and impredicative invariants, can be understood as merely derived forms in this base logic.

Secondly, I will show that our base logic is effective for formalization in Coq. I will show how to extend the Coq proof assistant with (spatial and non-spatial) named proof contexts and high-level tactics for reasoning in the Iris base logic. This way, we can seamlessly formalize the meta theory of the various layers of Iris, and use Iris for non-trivial applications such formalization of the Rust type system, (binary) logical relations, and concurrent data structures.

Sun 15 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00
Second Afternoon SessionTTT at Salle 105, Barre 44-54
Chair(s): Hugo Herbelin
Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq
Robbert Krebbers Delft University of Technology, Netherlands
Introducing MetaCoq: A Safe Tactic Language for Coq
Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina)
COST EUTypes session