TY - JOUR
T1 - MoSeL
T2 - A general, extensible modal framework for interactive proofs in separation logic
AU - Krebbers, Robbert
AU - Jourdan, Jacques Henri
AU - Jung, Ralf
AU - Tassarotti, Joseph
AU - Kaiser, Jan Oliver
AU - Timany, Amin
AU - Chargueraud, Arthur
AU - Dreyer, Derek
N1 - Publisher Copyright:
© 2018 author(s).
PY - 2018/9
Y1 - 2018/9
N2 - 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.
AB - 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.
KW - Coq Proof Assistant
KW - Interactive Theorem Proving
KW - Logic Of Bunched Implications
KW - Modal Logic
KW - Separation Logic
UR - http://www.scopus.com/inward/record.url?scp=85120104603&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85120104603&partnerID=8YFLogxK
U2 - 10.1145/3236772
DO - 10.1145/3236772
M3 - Article
AN - SCOPUS:85120104603
SN - 2475-1421
VL - 2
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - ICFP
M1 - 3236772
ER -