一句话：在 F* 的效果化依赖类型论中为并发分离逻辑给出语义，并据此构建可扩展的并发验证库。
近期研究致力于在类型论中建模效果。本文观察到效果化类型论可作为构建复杂编程构造与程序逻辑语义的基础，在 F* 证明助手中为并发分离逻辑（CSL）给出语义，使依赖类型且带效果的 F* 程序能使用并发并以可扩展的 CSL 进行规约与验证。与以往方法不同，作者直接从非确定性交错原子动作的效果语义中计算的指称，导出 CSL 的部分正确性 Hoare 规则。为展示灵活性，他们构建了通用且经验证的库，覆盖从动态分配的可存储自旋锁到协议索引通道等多种并发构造。结论是：该效果语义为分层构建面向已验证并发编程的领域特定语言与逻辑提供了简洁而有表达力的基础。
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself. Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F ⋆ proof assistant in a manner that enables dependently typed, effectful F ⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions. Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2111-15149,
title = {SteelCore: an extensible concurrent separation logic for effectful dependently typed programs},
author = {Nikhil Swamy and Aseem Rastogi and Aymeric Fromherz and Denis Merigoux and Danel Ahman and Guido Martínez},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3409003}
}