一句话：提出 MoSeL，一个通用可扩展的 Coq 框架，将 Iris 证明模式推广到更广泛的分离逻辑。
现有基于交互式证明助手的分离逻辑机械化工具中，Coq 的 Iris Proof Mode（IPM）提供了丰富策略，使证明接近普通 Coq 证明，但 IPM 与 Iris 特定逻辑绑定，适用范围受限。本文提出 MoSeL，一个通用、可扩展的 Coq 框架，将 IPM 的便利推广到更广泛的分离逻辑。与 IPM 不同，MoSeL 适用于仿射和线性分离逻辑及其组合，并提供可扩展的通用策略，以处理实例化逻辑特有的连接词。作者将 MoSeL 实例化到六种差异很大的分离逻辑，展示了其对交互式与半自动证明的有效策略支持。
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.
@article{paperbot298,
title = {MoSeL: a general, extensible modal framework for interactive proofs in separation logic},
author = {Robbert Krebbers and Jacques-Henri Jourdan and Ralf Jung and Joseph Tassarotti and Jan-Oliver Kaiser and Amin Timany and Arthur Charguéraud and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236772}
}