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

main
09:00 - 10:00: CoqPL 2017 - Opening Session at Auditorium
Chair(s): Emilio Jesús Gallego AriasMINES ParisTech
main09:00 - 10:00
Talk
Robbert KrebbersDelft University of Technology, Netherlands