CPP 2025 – Proceedings

14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025)

Frontmatter

Invited Talks

Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)
Emily Riehl
(John Hopkins University, USA)

Publisher's Version Article: poplws25cppmain-key1-p (type: Keynote) doi:10.1145/3703595.3710845

CRIS: The Power of Imagination in Specification and Verification (Invited Talk)
Chung-Kil Hur
(Seoul National University, South Korea)

Publisher's Version Article: poplws25cppmain-key2-p (type: Keynote) doi:10.1145/3703595.3710846

Papers

Leakage-Free Probabilistic Jasmin Programs
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, and Dominique Unruh
(INESC TEC, Portugal; University of Minho, Portugal; Tallinn University of Technology, Estonia; Input Output, Estonia; SandboxAQ, USA; University of Tartu, Estonia; RWTH Aachen University, Germany)

Publisher's Version Article: poplws25cppmain-p1-p (type: Full Paper) doi:10.1145/3703595.3705871

Leakage-Free Probabilistic Jasmin Programs (Video): Video of conference presentation

Nominal Matching Logic with Fixpoints
Mircea Sebe, Maribel Fernández, and James Cheney
(University of Illinois at Urbana-Champaign, USA; King’s College London, United Kingdom; University of Edinburgh, United Kingdom)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p9-p (type: Full Paper) doi:10.1145/3703595.3705872

	Nominal Matching Logic with Fixpoints (Video): Video of conference presentation
	NLML formalization (doi:10.1145/3580443): This artifact represents our attempts at formalizing Nominal Logic in Applicative Matching-mu Logic using the proof assistant Metamath Zero. It also presents our novel approach at deriving induction principles for languages with binders. To exemplify this, the formalization includes a definition of lambda calculus and ...

Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide
(RPTU Kaiserslautern-Landau, Germany; University of Bologna, Italy; Inria, France; Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p10-p (type: Full Paper) doi:10.1145/3703595.3705873

	Intrinsically Correct Sorting in Cubical Agda (Video): Video of conference presentation
	Intrinsically Correct Sorting in Cubical Agda (doi:10.5281/zenodo.14279034): This is the formalization accompanying the paper "Intrinsically Correct Sorting in Cubical Agda" (CPP2025).

Certifying Rings of Integers in Number Fields
Anne Baanen, Alain Chavarri Villarello, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands; Lean FRO, USA)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p11-p (type: Full Paper) doi:10.1145/3703595.3705874

	Certifying Rings of Integers in Number Fields (Video): Video of conference presentation
	Certifying rings of integers in number fields (doi:10.5281/zenodo.14283856): This repository contains the source code for the paper "Certifying rings of integers in number fields". Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with ...

Formalization of Differential Privacy in Isabelle/HOL
Tetsuya Sato and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)

Publisher's Version Article: poplws25cppmain-p18-p (type: Full Paper) doi:10.1145/3703595.3705875

Formalization of Differential Privacy in Isabelle/HOL (Video): Video of conference presentation

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Simon Friis Vindum, Aïna Linn Georges, and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p26-p (type: Full Paper) doi:10.1145/3703595.3705876

	The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic (Video): Video of conference presentation
	Artifact for The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic (doi:10.5281/zenodo.14285837): This is the artifact accompanying the paper "The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic". The artifact contains the Iris implementation of the nextgen modality.

Tactic Script Optimisation for Aesop
Jannis Limperg
(LMU Munich, Germany)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p30-p (type: Full Paper) doi:10.1145/3703595.3705877

	Tactic Script Optimisation for Aesop (Video): Video of conference presentation
	Supplement for "Tactic Script Optimisation for Aesop" (doi:10.5281/zenodo.14343543): The supplement contains (a) the specific version of Aesop described in the paper; (b) all code necessary to reproduce the benchmarks described in the paper; (c) the benchmark data reported in the paper.

A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)

Publisher's Version Article: poplws25cppmain-p43-p (type: Full Paper) doi:10.1145/3703595.3705878

A CHERI C Memory Model for Verified Temporal Safety (Video): Video of conference presentation

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, and Bas Spitters
(Aarhus University, Denmark)

Publisher's Version Article: poplws25cppmain-p44-p (type: Full Paper) doi:10.1145/3703595.3705879

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq (Video): Video of conference presentation

Formally Verified Hardening of C Programs against Hardware Fault Injection
Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet
(Ecole Nationale de l’Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France)

Publisher's Version Article: poplws25cppmain-p52-p (type: Full Paper) doi:10.1145/3703595.3705880

Formally Verified Hardening of C Programs against Hardware Fault Injection (Video): Video of conference presentation

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk and Aart Middeldorp
(University of Innsbruck, Austria)

Publisher's Version Info Article: poplws25cppmain-p55-p (type: Full Paper) doi:10.1145/3703595.3705881

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems (Video): Video of conference presentation

An Isabelle/HOL Framework for Synthetic Completeness Proofs
Asta Halkjær From
(University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p64-p (type: Full Paper) doi:10.1145/3703595.3705882

	An Isabelle/HOL Framework for Synthetic Completeness Proofs (Video): Video of conference presentation
	Formalization for An Isabelle/HOL Framework for Synthetic Completeness Proofs (doi:10.5281/zenodo.14278854): The Isabelle/HOL theory files behind the paper.

Formalized Burrows-Wheeler Transform
Louis Cheung, Alistair Moffat, and Christine Rizkallah
(University of Melbourne, Australia)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p80-p (type: Full Paper) doi:10.1145/3703595.3705883

	Formalized Burrows-Wheeler Transform (Video): Video of conference presentation
	Formalized Burrows-Wheeler Transform (doi:10.5281/zenodo.14279882): This is a formalization of the Burrows-Wheeler Transform and its inverse in Isabelle/HOL.

Verified and Efficient Matching of Regular Expressions with Lookaround
Agnishom Chattopadhyay, Angela W. Li, and Konstantinos Mamouras
(Rice University, USA)

Publisher's Version Article: poplws25cppmain-p85-p (type: Full Paper) doi:10.1145/3703595.3705884

Verified and Efficient Matching of Regular Expressions with Lookaround (Video): Video of conference presentation

Machine Checked Proofs and Programs in Algebraic Combinatorics
Florent Hivert
(University Paris-Saclay - LISN - LMF - CNRS - Inria, France)

Publisher's Version Info Article: poplws25cppmain-p87-p (type: Full Paper) doi:10.1145/3703595.3705885

Machine Checked Proofs and Programs in Algebraic Combinatorics (Video): Video of conference presentation

Further Tackling Post Correspondence Problem and Proof Generation
Akihiro Omori and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)

Publisher's Version Article: poplws25cppmain-p93-p (type: Full Paper) doi:10.1145/3703595.3705886

Further Tackling Post Correspondence Problem and Proof Generation (Video): Video of conference presentation

Formalizing the One-Way to Hiding Theorem
Katharina Heidler and Dominique Unruh
(TU Munich, Germany; RWTH Aachen University, Germany; University of Tartu, Estonia)

Publisher's Version Article: poplws25cppmain-p98-p (type: Full Paper) doi:10.1145/3703595.3705887

Formalizing the One-Way to Hiding Theorem (Video): Video of conference presentation

Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon, Chuta Sano, Alberto Momigliano, and Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p120-p (type: Full Paper) doi:10.1145/3703595.3705888

Split Decisions: Explicit Contexts for Substructural Languages (Video): Video of conference presentation

Split Decisions: Explicit Contexts for Substructural Languages (artifact) (doi:10.5281/zenodo.14271731): This is an artifact supporting the paper "Split Decisions: Explicit Contexts for Substructural Languages" (CPP 2025). The artifact contains an implementation in Beluga of CARVe, a general infrastructure for encoding substructural systems and reasoning about their meta-theory. It also includes encodings of several case ...

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
(University of Innsbruck, Austria; JAIST, Japan; AIST, Japan)

Publisher's Version Info Article: poplws25cppmain-p127-p (type: Full Paper) doi:10.1145/3703595.3705889

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting (Video): Video of conference presentation

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski
(ENS de Lyon - CNRS - Inria - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France; CNRS - ENS de Lyon - Inria - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France; Inria - CNRS - ENS de Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France)

Publisher's Version Article: poplws25cppmain-p162-p (type: Full Paper) doi:10.1145/3703595.3705890

Monadic Interpreters for Concurrent Memory Models (Video): Video of conference presentation

proc time: 0.06