POPL 2025 Co-Located Events
POPL 2025 Co-Located Events

Powered by

Conference Publishing Consulting

14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), January 20-21, 2025, Denver, CO, USA

CPP 2025 – Preliminary Table of Contents

Contents - Abstracts - Authors

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

Frontmatter

Message from the Chairs

Papers

Leakage-Free Probabilistic Jasmin Programs
Denis Firsov, Tiago Oliveira, José Bacelar Almeida, and Dominique Unruh
(Tallinn University of Technology, Estonia; SandboxAQ, n.n.; HASLab, n.n.; INESC TEC, Portugal; University of Minho, Portugal; University of Tartu, Estonia)

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)

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; Radboud University Nijmegen, Netherlands)

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

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

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; MPI-SWS, Germany)

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

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)

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

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; CNRS, France)

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

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

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

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

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

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

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

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

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

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski
(Inria - LIP, France; CNRS, France; Inria, France)

proc time: 4.56