一句话：在依赖类型语言 F* 中提出 Steel，用五元组 Hoare 逻辑把并发程序与其分离逻辑证明协同开发。
Steel 是一个嵌入在依赖类型编程语言与证明助手 F* 中的并发程序开发与验证语言，其基础是 SteelCore——一个在 F* 中形式化的并发分离逻辑（CSL）。论文关注如何把该逻辑的证明规则以支持程序与证明协同开发的形式暴露出来。主要贡献是提出一种新型的五元组 Hoare 逻辑，同时包含分离逻辑与一阶逻辑成分，从而支持高效的验证条件（VC）生成，并通过策略与 SMT 求解相结合来消解证明义务。作者进一步把五元组系统产生的 VC 归约为求解一组结合-交换（AC）合一的约束，并设计了策略，在可交由 SMT 消解的等式模意义下对 AC 匹配约束进行（部分）求解。该系统已在 F* 中完全机械化实现。作者通过若干验证过的程序与库进行评估，包括顺序与并发链表数据结构、证明库以及一个双方会话类型库，结果表明该体系能混合使用自动化与交互式证明，从而高效地构造出基于最先进、高表达力 CSL 的根基性验证程序。
Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.
@article{paperbot1140,
title = {Steel: proof-oriented programming in a dependently typed concurrent separation logic},
author = {Aymeric Fromherz and Aseem Rastogi and Nikhil Swamy and Sydney Gibson and Guido Martínez and Denis Merigoux and Tahina Ramananandro},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473590}
}