CPP 2025 – Preliminary Table of Contents

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

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

Publisher's Version

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

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

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

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

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

Publisher's Version

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

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

Publisher's Version Published Artifact Artifacts Available

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

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

Publisher's Version

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

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

Publisher's Version Info

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

Publisher's Version Published Artifact Artifacts Available

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

Publisher's Version Published Artifact Artifacts Available

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

Publisher's Version

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

Publisher's Version Info

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

Publisher's Version

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

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

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

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

proc time: 6.23