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

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

14:20 - 16:00
Concurrency 1POPL at Auditorium
Chair(s): Ilya Sergey University College London
14:20
25m
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached
14:45
25m
Talk
Automatically Comparing Memory Consistency Models
POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached
15:10
25m
Talk
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached
15:35
25m
Talk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University