POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 15:10 - 15:35 at Auditorium - Concurrency 1 Chair(s): Ilya Sergey

When using a proof assistant to reason in an embedded logic – like separation logic – one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic.

In this paper, we introduce IPM: ``Interactive Proof Mode for embedded logics in Coq'', a novel method for extending the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we are able to implement high-level tactics for introduction and elimination of all connectives of the object logic, and thereby make reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We apply our method to Iris: a state of the art higher-order impredicative concurrent separation logic.

We show that IPM is very general, and – in contrast to earlier work – is not just limited to program verification. We demonstrate its generality by formalizing correctness proofs of fine-grained concurrent algorithms, derived constructs of the Iris logic, and a unary and binary logical relation for a language with concurrency, higher-order store, polymorphism, and recursive types. This is the first formalization of a binary logical relation for such an expressive language. We also show how to use the logical relation to prove contextual refinement of fine-grained concurrent algorithms.

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: Concurrency 1POPL at Auditorium
Chair(s): Ilya SergeyUniversity College London
14:20 - 14:45
A Promising Semantics for Relaxed-Memory Concurrency
Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS
Link to publication Pre-print Media Attached
14:45 - 15:10
Automatically Comparing Memory Consistency Models
John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK
Pre-print Media Attached File Attached
15:10 - 15:35
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University
DOI Pre-print Media Attached
15:35 - 16:00
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University