Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 13:00 - 13:22 at Stifel Theatre - Proof Techniques and Mechanization Chair(s): Niki Vazou

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 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30: Proof Techniques and MechanizationResearch Papers at Stifel Theatre
Chair(s): Niki VazouUniversity of Maryland, USA
13:00 - 13:22
Talk
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Research Papers
Robbert KrebbersDelft University of Technology, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Ralf JungMPI-SWS, Joseph TassarottiCarnegie Mellon University, Jan-Oliver KaiserMPI-SWS, Amin Timanyimec-Distrinet KU-Leuven, Arthur CharguéraudInria, Derek DreyerMPI-SWS
DOI
13:22 - 13:45
Talk
Mtac2: Typed Tactics for Backward Reasoning in Coq
Research Papers
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET, Robbert KrebbersDelft University of Technology, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek DreyerMPI-SWS
DOI
13:45 - 14:07
Talk
Compositional Soundness Proofs of Abstract Interpreters
Research Papers
Sven KeidelDelft University of Technology, Netherlands, Casper Bach PoulsenDelft University of Technology, Sebastian ErdwegDelft University of Technology, Netherlands
DOI
14:07 - 14:30
Talk
Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper
Research Papers
Nicolas TabareauInria, Éric TanterUniversity of Chile & Inria Paris, Matthieu SozeauInria
DOI