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
Title Page
Message from the Chairs
Committees
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)
Article Search
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)
Article Search
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)
Article Search
Certifying Rings of Integers in Number Fields
Anne Baanen
,
Alain Chavarri Villarello
, and
Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands; Lean FRO, Netherlands)
Article Search
Formalization of Differential Privacy in Isabelle/HOL
Tetsuya Sato
and
Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
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)
Article Search
Tactic Script Optimisation for Aesop
Jannis Limperg
(LMU Munich, Germany)
Article Search
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)
Article Search
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen,
Jean Pichon-Pharabod
, and
Bas Spitters
(Aarhus University, Denmark)
Article Search
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)
Article Search
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk
and
Aart Middeldorp
(University of Innsbruck, Austria)
Article Search
An Isabelle/HOL Framework for Synthetic Completeness Proofs
Asta Halkjær From
(University of Copenhagen, Denmark)
Article Search
Formalized Burrows-Wheeler Transform
Louis Cheung
,
Alistair Moffat
, and
Christine Rizkallah
(University of Melbourne, Australia)
Article Search
Verified and Efficient Matching of Regular Expressions with Lookaround
Agnishom Chattopadhyay
,
Angela W. Li
, and
Konstantinos Mamouras
(Rice University, USA)
Article Search
Machine Checked Proofs and Programs in Algebraic Combinatorics
Florent Hivert
(University Paris-Saclay - LISN - LMF - CNRS - Inria, France)
Article Search
Further Tackling Post Correspondence Problem and Proof Generation
Akihiro Omori
and
Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
Formalizing the One-Way to Hiding Theorem
Katharina Heidler
and
Dominique Unruh
(TU Munich, Germany; RWTH Aachen University, Germany)
Article Search
Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon
,
Chuta Sano
,
Alberto Momigliano
, and
Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)
Article Search
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)
Article Search
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)
Article Search
proc time: 0.7