Tahina Ramananandro > Research >

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

Gabriel Ebner (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Guido Martínez (RiSE)
Aseem Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Thibault Dardinier (Programming Methodology Group, ETH Zürich, Switzerland)
Megan Frisella (Programming Languages and Software Engineering and Systems for Future Intelligence, Paul G. Allen School, University of Washington, Seattle, WA, USA)
Tahina Ramananandro (RiSE)
Nikhil Swamy (RiSE)

PLDI 2025

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.