POPL 2025 (series) / CPP 2025 (series) /
CPP 2025 Program
This is the CPP 2025 program - see the full program for POPL 2025 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Prospects for Computer Formalization of Infinite-Dimensional Category Theory CPP Emily Riehl Johns Hopkins University | ||
10:00 30mTalk | Certifying rings of integers in number fieldsdistinguished paperremote presentation CPP Anne Baanen Vrije Universiteit Amsterdam, Alain Chavarri Villarello Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam | ||
11:00 - 12:30 | |||
11:00 30mTalk | Split Decisions: Explicit Contexts for Substructural Languagesdistinguished paper CPP Daniel Zackon McGill University, Chuta Sano McGill University, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University Link to publication DOI | ||
11:30 30mTalk | Machine Checked Proofs and Programs in Algebraic Combinatorics CPP Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA | ||
12:00 30mTalk | Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IRremote presentation CPP Nicolas Chappe Inria Lyon, LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski Inria | ||
14:00 - 15:30 | |||
14:00 30mTalk | An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting CPP Dohan Kim University of Innsbruck, Teppei Saito Japan Advanced Institute of Science and Technology, Japan, René Thiemann University of Innsbruck, Akihisa Yamada National Institute of Informatics | ||
14:30 30mTalk | Intrinsically Correct Sorting in Cubical Agda CPP Cass Alexandru RPTU Kaiserslautern-Landau, Vikraman Choudhury Università di Bologna & Inria OLAS, Jurriaan Rot Radboud University Nijmegen, Niels van der Weide Radboud University | ||
15:00 30mTalk | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems CPP | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalized Burrows-Wheeler Transform CPP Louis Cheung University of Melbourne, Alistair Moffat The University of Melbourne, Christine Rizkallah University of Melbourne | ||
16:30 30mTalk | Verified and Efficient Matching of Regular Expressions with Lookaroundremote presentation CPP | ||
17:00 30mTalk | Further Tackling Post Correspondence Problem and Proof Generation CPP Akihiro Omori Department of Mathematical and Computing Science, Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology | ||
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | CRIS: The power of imagination in specification and verification CPP | ||
10:00 30mTalk | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logicdistinguished paper CPP Simon Friis Vindum Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Lars Birkedal Aarhus University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Leakage-Free Probabilistic Jasmin Programs CPP Denis Firsov Tallinn University of Technology, Tiago Oliveira SandboxAQ, José Bacelar Almeira University of Minho & INESC TEC, Dominique Unruh RWTH Aachen | ||
11:30 30mTalk | Formally verified hardening of C programs against hardware fault injection CPP Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC), Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux CNRS, Marie-Laure Potet Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Pre-print | ||
12:00 30mTalk | CertiCoq-Wasm: A verified WebAssembly backend for CertiCoqremote presentation CPP Wolfgang Meier Aarhus University, Martin Jensen Aarhus University, Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | Nominal Matching Logic With Fixpoints CPP | ||
14:30 30mTalk | Tactic Script Optimisation for Aesop CPP Jannis Limperg University of Munich (LMU) Link to publication DOI | ||
15:00 30mTalk | An Isabelle/HOL Framework for Synthetic Completeness Proofsremote presentation CPP Asta Halkjær From University of Copenhagen DOI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalization of Differential Privacy in Isabelle/HOL CPP | ||
16:30 30mTalk | A CHERI C Memory Model for Verified Temporal Safety CPP Vadim Zaliva University of Cambridge, UK, Kayvan Memarian University of Cambridge, Brian Campbell University of Edinburgh, Ricardo Almeida University of Edinburgh, Nathaniel Filardo University of Cambridge, Ian Stark The University of Edinburgh, Peter Sewell University of Cambridge | ||
17:00 30mTalk | Formalizing the One-way to Hiding Theorem CPP | ||
17:30 - 18:00 | |||
17:30 30mMeeting | Business Meeting CPP | ||