POPL 2024 Co-Located Events
POPL 2024 Co-Located Events
Powered by
Conference Publishing Consulting

13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), January 15-16, 2024, London, UK

CPP 2024 – Proceedings

Contents - Abstracts - Authors

13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024)


Title Page
Welcome from the Chairs


Under-Approximation for Scalable Bug Detection (Keynote)
Azalea RaadORCID logo
(Imperial College London, UK)
Publisher's Version


UTC Time, Formally Verified
Ana de Almeida BorgesORCID logo, Mireia González Bedmar ORCID logo, Juan Conejero Rodríguez ORCID logo, Eduardo Hermo Reyes ORCID logo, Joaquim Casals Buñuel ORCID logo, and Joost J. Joosten ORCID logo
(University of Barcelona, Spain; Formal Vindications, Spain)
Publisher's Version Published Artifact Info Artifacts Available
VCFloat2: Floating-Point Error Analysis in Coq
Andrew W. AppelORCID logo and Ariel E. Kellison ORCID logo
(Princeton University, USA; Cornell University, USA)
Publisher's Version
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter ORCID logo, Benjamin Salling Hvass ORCID logo, Lasse Letager Hansen ORCID logo, Théo Winterhalter ORCID logo, Cătălin Hriţcu ORCID logo, and Bas Spitters ORCID logo
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
Publisher's Version
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan ZhaoORCID logo, George PîrleaORCID logo, Zhendong Ang ORCID logo, Umang Mathur ORCID logo, and Ilya SergeyORCID logo
(National University of Singapore, Singapore)
Publisher's Version Published Artifact Info Artifacts Available
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than NguyenORCID logo, Lennart Beringer ORCID logo, William ManskyORCID logo, and Shengyi Wang ORCID logo
(University of Illinois at Chicago, USA; Princeton University, USA)
Publisher's Version Published Artifact Artifacts Available
Unification for Subformula Linking under Quantifiers
Ike MulderORCID logo and Robbert KrebbersORCID logo
(Radboud University Nijmegen, Netherlands)
Publisher's Version
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon ORCID logo, Frédéric Besson ORCID logo, and Tristan Ninet ORCID logo
(Inria - University of Rennes, France; Thales, France)
Publisher's Version
Memory Simulations, Security and Optimization in a Verified Compiler
David MonniauxORCID logo
(University of Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France)
Publisher's Version
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko ORCID logo, Margus VeanesORCID logo, and Gabriel Ebner ORCID logo
(Tallinn University of Technology, Estonia; Microsoft Research, USA)
Publisher's Version
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Chelsea Edmonds ORCID logo and Lawrence C. Paulson ORCID logo
(University of Sheffield, UK; University of Cambridge, UK)
Publisher's Version Info
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa ORCID logo, Dohan Kim ORCID logo, Kiraku Shintani ORCID logo, and René Thiemann ORCID logo
(JAIST, Japan; University of Innsbruck, Austria)
Publisher's Version Info
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White ORCID logo, Laura TitoloORCID logo, J. Tanner Slagel ORCID logo, and César Muñoz ORCID logo
Publisher's Version
Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
Siddhartha Gadgil ORCID logo and Anand Rao Tadipatri ORCID logo
(Indian Institute of Science, India; Indian Institute of Science Education and Research, India)
Publisher's Version
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de Frutos-FernándezORCID logo and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio ORCID logo
(Autonomous University of Madrid, Spain; Université Jean Monnet Saint-Étienne, France)
Publisher's Version Info
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Joseph Eremondi ORCID logo
(University of Edinburgh, UK)
Publisher's Version Info
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Ian Shillito ORCID logo and Dominik Kirst ORCID logo
(Australian National University, Australia; Ben-Gurion University of the Negev, Israel)
Publisher's Version
Martin-Löf à la Coq
Arthur Adjedj ORCID logo, Meven Lennon-Bertrand ORCID logo, Kenji Maillard ORCID logo, Pierre-Marie Pédrot ORCID logo, and Loïc Pujet ORCID logo
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
Publisher's Version Published Artifact Artifacts Available
Univalent Double Categories
Niels van der WeideORCID logo, Nima Rasekh ORCID logo, Benedikt AhrensORCID logo, and Paige Randall North ORCID logo
(Radboud University Nijmegen, Netherlands; Max Planck Institute for Mathematics, Germany; Delft University of Technology, Netherlands; University of Birmingham, UK; Utrecht University, Netherlands)
Publisher's Version
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt AhrensORCID logo, Ralph MatthesORCID logo, Niels van der WeideORCID logo, and Kobe Wullaert ORCID logo
(Delft University of Technology, Netherlands; University of Birmingham, UK; IRIT - Université de Toulouse - CNRS - Toulouse INP - UT3, France; Radboud University Nijmegen, Netherlands)
Publisher's Version
Formalizing the ∞-Categorical Yoneda Lemma
Nikolai Kudasov ORCID logo, Emily Riehl ORCID logo, and Jonathan Weinberger ORCID logo
(Innopolis University, Russia; Johns Hopkins University, USA)
Publisher's Version Published Artifact Info Artifacts Available

proc time: 5.16