About

The Clutch project is a family of program logics for reasoning about higher-order probabilistic programs. It builds on the Iris separation logic framework in the Rocq Prover. The included logics can be used for verifying properties such as contextual equivalence, error bounds, expected cost, almost-sure termination, and differential privacy.

The source code, including all variants developed in the publications below, lives in the logsem/clutch repository.

Logics and Examples

See the Logics and Examples page for an overview of the logics in the project and the examples verified with them.

Events

• 11 May–15 May 2026: Lectures on Verifying Probabilistic Programs with Separation Logic at EPIT 2026, CIRM, Marseille, France
• 11 January 2026: Tutorial on probabilistic program verification at POPL, Rennes, France

Publications

Below is an overview of publications based on the Clutch framework.

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic

Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal
In PLDI 2026: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Extended version Rocq development Rocq artifact

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs

Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
In PLDI 2026: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Rocq artifact

Specifications and Implementations of Random Samplers in Higher-Order Separation Logic

Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal
In CPP 2026: ACM SIGPLAN Conference on Certified Programs and Proofs

.pdf Rocq development Artifact

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs

Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Markus de Medeiros, Joseph Tassarotti, Lars Birkedal
In ICFP 2025: ACM SIGPLAN International Conference on Functional Programming

.pdf

Approximate Relational Reasoning for Higher-Order Probabilistic Programs

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
In POPL 2025: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Artifact

Tachis: Higher-Order Separation Logic with Credits for Expected Costs

Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Artifact Rocq development

Almost-Sure Termination by Guarded Refinement

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming

.pdf Artifact Rocq development

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming
Recipient of ICFP 2024 Distinguished Paper Award

.pdf Artifact Rocq development

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Extended version Rocq development Artifact