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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00
|A Promising Semantics for Relaxed-Memory Concurrency|
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWSLink to publication Pre-print Media Attached
|Automatically Comparing Memory Consistency Models|
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UKPre-print Media Attached File Attached
|Interactive Proofs in Higher-Order Concurrent Separation Logic|
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus UniversityDOI Pre-print Media Attached
|A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic|