Print Email Facebook Twitter MoSeL Title MoSeL: A general, extensible modal framework for interactive proofs in separation logic Author Krebbers, R.J. (TU Delft Programming Languages) Jourdan, Jacques-Henri (University of Paris-Sud; University Paris-Saclay) Jung, Ralf (Max Planck Institute for Software Systems (MPI-SWS)) Tassarotti, Joseph (Carnegie Mellon University) Kaiser, Jan-Oliver (Max Planck Institute for Software Systems (MPI-SWS)) Timany, Amin (Katholieke Universiteit Leuven; IMEC) Charguéraud, Arthur (University of Strasbourg; CNRS) Dreyer, Derek (Max Planck Institute for Software Systems (MPI-SWS)) Date 2018 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. To reference this document use: http://resolver.tudelft.nl/uuid:3e97600a-6d9a-4e86-b564-bdeb9c150d7a DOI https://doi.org/10.1145/3236772 ISSN 2475-1421 Source Proceedings of the ACM on Programming Languages, 2 (ICFP), 77:1-77:30 Part of collection Institutional Repository Document type journal article Rights © 2018 R.J. Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer Files PDF 47928926_icfp18main_p41_p.pdf 559 KB Close viewer /islandora/object/uuid:3e97600a-6d9a-4e86-b564-bdeb9c150d7a/datastream/OBJ/view