MoSeL: a general, extensible modal framework for interactive proofs in separation logic
In: International Conference on Functional Programming (ICFP 2018) ; https://hal.archives-ouvertes.fr/hal-01898522 ; International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩ ; https://conf.researchr.org/home/icfp-2018, 2018
Online
Konferenz
Zugriff:
International audience ; 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.
| Titel: |
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
|
|---|---|
| Autor/in / Beteiligte Person: | Krebbers, Robbert ; Jourdan, Jacques-Henri ; Jung, Ralf ; Tassarotti, Joseph ; Kaiser, Jan-Oliver ; Timany, Amin ; Charguéraud, Arthur ; Dreyer, Derek ; Delft University of Technology (TU Delft) ; Laboratoire de Recherche en Informatique (LRI) ; CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS) ; Paris-Saclay, Université ; Max Planck Institute for Software Systems (MPI-SWS) ; Carnegie Mellon University Pittsburgh (CMU) ; Distributed Systems and Computer Networks (DistriNet) ; Catholic University of Leuven - Katholieke Universiteit Leuven (KU Leuven) ; Université de Strasbourg (UNISTRA) ; Compilation pour les Architectures MUlti-coeurS (CAMUS) ; Inria Nancy - Grand Est ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube) ; École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et nanosciences d'Alsace (FMNGE) ; Institut de Chimie du CNRS (INC)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Centre National de la Recherche Scientifique (CNRS)-Institut de Chimie du CNRS (INC)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique ; Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg) ; Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA) ; ACM ; ANR-15-CE25-0008,VOCAL,Bibliothèque OCaml vérifiée(2015) ; European Project: 683289,H2020,ERC-2015-CoG,RustBelt(2016) |
| Link: | |
| Zeitschrift: | International Conference on Functional Programming (ICFP 2018) ; https://hal.archives-ouvertes.fr/hal-01898522 ; International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩ ; https://conf.researchr.org/home/icfp-2018, 2018 |
| Veröffentlichung: | HAL CCSD ; ACM, 2018 |
| Medientyp: | Konferenz |
| DOI: | 10.1145/3236772 |
| Schlagwort: |
|
| Sonstiges: |
|