一句话：提出 PulseCore，一个面向依赖类型高阶并发程序内在证明的并发分离逻辑，并在 F* 中机械化验证。
PulseCore 是一种新的程序逻辑，旨在为高阶、有状态、并发且依赖类型的程序提供内在证明。它具备现代并发分离逻辑的诸多特性，包括动态分配的非直谓不变量、高阶幽灵状态、带 later credits 的步进索引，以及对用户自定义幽灵状态构造的支持。PulseCore 在 F* 中基础性地开发，所有证明完全机械化，并可直接应用于 F* 程序。为评估其表达力与实用性，作者使用 F* 中的表面语言 Pulse 开发了一系列程序证明，涵盖 OCaml5 风格任务池及其并行程序、多种数据结构和同步原语、需要高阶幽灵状态的屏障，以及 DICE 保护环境这一工业标准安全启动协议的验证实现。评估总计超过 31,000 行验证代码，表明 PulseCore 既高度表达力强，又适用于多种程序证明场景。
PulseCore is a new program logic suitable for intrinsic proofs of higher-order, stateful, concurrent, dependently typed programs. It provides many of the features of a modern, concurrent separation logic, including dynamically allocated impredicative invariants, higher-order ghost state, step-indexing with later credits, and support for user-defined ghost state constructions. PulseCore is developed foundationally within the F ⋆ programming language with fully mechanized proofs, and is applicable to F ⋆ programs itself. To evaluate our work, we use Pulse , a surface language within F ⋆ for PulseCore , to develop a range of program proofs. Illustrating its suitability for proving higher-order concurrent programs, we present a verified library for task pools in the style of OCaml5, together with some verified task-parallel programs. Next, we present various data structures and synchronization primitives, including a barrier that requires the use of higher-order ghost state. Finally, we present a verified implementation of the DICE Protection Environment, an industry standard secure boot protocol. Taken together, our evaluation consists of more than 31,000 lines of verified code in a range of settings, providing evidence that PulseCore is both highly expressive as well as practical for a variety of program proof applications.
@article{paperbot3104,
title = {PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs},
author = {Gabriel Ebner and Guido Martínez and Aseem Rastogi and Thibault Dardinier and Megan Frisella and Tahina Ramananandro and Nikhil Swamy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729311}
}