Invited Talk -- Demonstration of the Iris separation logic in Coq
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
|09:00 - 10:00|
Robbert KrebbersDelft University of Technology, Netherlands