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 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 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 doi:10.1145/3703595.3705871

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 doi:10.1145/3703595.3705872

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 doi:10.1145/3703595.3705873

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 doi:10.1145/3703595.3705874

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

Publisher's Version Article: poplws25cppmain-p18-p doi:10.1145/3703595.3705875

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 doi:10.1145/3703595.3705876

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

Publisher's Version Published Artifact Artifacts Available Article: poplws25cppmain-p30-p doi:10.1145/3703595.3705877

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 doi:10.1145/3703595.3705878

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 doi:10.1145/3703595.3705879

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 doi:10.1145/3703595.3705880

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 doi:10.1145/3703595.3705881

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 doi:10.1145/3703595.3705882

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 doi:10.1145/3703595.3705883

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 doi:10.1145/3703595.3705884

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 doi:10.1145/3703595.3705885

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 doi:10.1145/3703595.3705886

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 doi:10.1145/3703595.3705887

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 doi:10.1145/3703595.3705888

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 doi:10.1145/3703595.3705889

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 doi:10.1145/3703595.3705890

proc time: 108.6