MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs. However, IPM is tied to a particular separation logic (namely, Iris), thus limiting its applicability.
In this paper, we propose MoSeL, a general and extensible Coq framework that brings the benefits of IPM to a much larger class of separation logics. Unlike IPM, MoSeL is applicable to both affine and linear separation logics (and combinations thereof), and provides generic tactics that can be easily extended to account for the bespoke connectives of the logics with which it is instantiated. To demonstrate the effectiveness of MoSeL, we have instantiated it to provide effective tactical support for interactive and semi-automated proofs in six very different separation logics.
Tue 25 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:00 - 14:30
Proof Techniques and MechanizationResearch Papers at Stifel Theatre
Chair(s): Niki Vazou University of Maryland, USA
|MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic|
Robbert Krebbers Delft University of Technology, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Ralf Jung MPI-SWS, Joseph Tassarotti Carnegie Mellon University, Jan-Oliver Kaiser MPI-SWS, Amin Timany imec-Distrinet KU-Leuven, Arthur Charguéraud Inria, Derek Dreyer MPI-SWSDOI
|Mtac2: Typed Tactics for Backward Reasoning in Coq|
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET, Robbert Krebbers Delft University of Technology, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek Dreyer MPI-SWSDOI
|Compositional Soundness Proofs of Abstract Interpreters|
Sven Keidel Delft University of Technology, Netherlands, Casper Bach Poulsen Delft University of Technology, Sebastian Erdweg Delft University of Technology, NetherlandsDOI
|Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper|
Nicolas Tabareau Inria, Éric Tanter University of Chile & Inria Paris, Matthieu Sozeau InriaDOI