Standard

MoSeL : A general, extensible modal framework for interactive proofs in separation logic. / Krebbers, Robbert; Jourdan, Jacques-Henri; Jung, Ralf; Tassarotti, Joseph; Kaiser, Jan-Oliver; Timany, Amin; Charguéraud, Arthur; Dreyer, Derek.

In: Proceedings of the ACM on Programming Languages, Vol. 2, No. ICFP, 77, 2018, p. 77:1-77:30.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

Krebbers, R, Jourdan, J-H, Jung, R, Tassarotti, J, Kaiser, J-O, Timany, A, Charguéraud, A & Dreyer, D 2018, 'MoSeL: A general, extensible modal framework for interactive proofs in separation logic' Proceedings of the ACM on Programming Languages, vol. 2, no. ICFP, 77, pp. 77:1-77:30. https://doi.org/10.1145/3236772

APA

Krebbers, R., Jourdan, J-H., Jung, R., Tassarotti, J., Kaiser, J-O., Timany, A., ... Dreyer, D. (2018). MoSeL: A general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages, 2(ICFP), 77:1-77:30. [77]. https://doi.org/10.1145/3236772

Vancouver

Krebbers R, Jourdan J-H, Jung R, Tassarotti J, Kaiser J-O, Timany A et al. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages. 2018;2(ICFP):77:1-77:30. 77. https://doi.org/10.1145/3236772

Author

Krebbers, Robbert ; Jourdan, Jacques-Henri ; Jung, Ralf ; Tassarotti, Joseph ; Kaiser, Jan-Oliver ; Timany, Amin ; Charguéraud, Arthur ; Dreyer, Derek. / MoSeL : A general, extensible modal framework for interactive proofs in separation logic. In: Proceedings of the ACM on Programming Languages. 2018 ; Vol. 2, No. ICFP. pp. 77:1-77:30.

BibTeX

@article{3e97600a6d9a4e86b564bdeb9c150d7a,
title = "MoSeL: A general, extensible modal framework for interactive proofs in separation logic",
abstract = "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.",
author = "Robbert Krebbers and Jacques-Henri Jourdan and Ralf Jung and Joseph Tassarotti and Jan-Oliver Kaiser and Amin Timany and Arthur Chargu{\'e}raud and Derek Dreyer",
year = "2018",
doi = "10.1145/3236772",
language = "Undefined/Unknown",
volume = "2",
pages = "77:1--77:30",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
number = "ICFP",

}

RIS

TY - JOUR

T1 - MoSeL

T2 - Proceedings of the ACM on Programming Languages

AU - Krebbers, Robbert

AU - Jourdan, Jacques-Henri

AU - Jung, Ralf

AU - Tassarotti, Joseph

AU - Kaiser, Jan-Oliver

AU - Timany, Amin

AU - Charguéraud, Arthur

AU - Dreyer, Derek

PY - 2018

Y1 - 2018

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.

U2 - 10.1145/3236772

DO - 10.1145/3236772

M3 - Article

VL - 2

SP - 77:1-77:30

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - ICFP

M1 - 77

ER -

ID: 47928926