Sites Inria

English version

Séminaire des équipes de recherche

MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic

© INRIA Sophie Auvin - G comme Grille

A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant.

  • Date : 10/09/2018
  • Lieu : Inria de Paris, 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Jacques-Louis Lions 1, bâtiment C
  • Intervenant(s) : Robbert Krebbers (Delft University of Technology)

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 talk, I will describe 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.

MoSeL is joint work with Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer.

Mots-clés : MoSeL Inria de Paris Extensible Framework Interactive Proofs Séminaire Gallium Modal Separation Logic

Haut de page

Suivez Inria