POPL 2017
Sun 15 - Sat 21 January 2017
Sat 21 Jan 2017 09:00 - 10:00 at Auditorium - Opening Session Chair(s): Emilio Jesús Gallego Arias

I will demonstrate the Coq formalization of Iris – a framework for higher-order concurrent separation logic. A novel feature of the Coq formalization of Iris is its support for interactive proofs in the logic. We have achieved that by extending Coq with spatial and non-spatial named contexts for the hypotheses of Iris. Using these contexts we have implemented Coq-like tactics for reasoning in the Iris logic. In this talk, I will discuss the Coq implementation of Iris and demonstrate how it can be used for verification of sequential and concurrent programs.

Sat 21 Jan

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

09:00 - 10:00
Opening SessionCoqPL at Auditorium
Chair(s): Emilio Jesús Gallego Arias MINES ParisTech
09:00
60m
Talk
Invited Talk -- Demonstration of the Iris separation logic in Coq
CoqPL
I: Robbert Krebbers Delft University of Technology, Netherlands