CPP 2024 – Proceedings

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

Frontmatter

Keynote

Under-Approximation for Scalable Bug Detection (Keynote)
Azalea Raad
(Imperial College London, UK)

Publisher's Version

Papers

UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)

Publisher's Version Published Artifact Info Artifacts Available

VCFloat2: Floating-Point Error Analysis in Coq
Andrew W. Appel and Ariel E. Kellison
(Princeton University, USA; Cornell University, USA)

Publisher's Version

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)

Publisher's Version

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(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 Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang
(University of Illinois at Chicago, USA; Princeton University, USA)

Publisher's Version Published Artifact Artifacts Available

Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)

Publisher's Version

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon, Frédéric Besson, and Tristan Ninet
(Inria - University of Rennes, France; Thales, France)

Publisher's Version

Memory Simulations, Security and Optimization in a Verified Compiler
David Monniaux
(University of Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France)

Publisher's Version

Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner
(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 and Lawrence C. Paulson
(University of Sheffield, UK; University of Cambridge, UK)

Publisher's Version Info

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann
(JAIST, Japan; University of Innsbruck, Austria)

Publisher's Version Info

A Temporal Differential Dynamic Logic Formal Embedding
Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz
(NASA, USA; AMA, USA)

Publisher's Version

Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
Siddhartha Gadgil and Anand Rao Tadipatri
(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ández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
(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
(University of Edinburgh, UK)

Publisher's Version Info

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Ian Shillito and Dominik Kirst
(Australian National University, Australia; Ben-Gurion University of the Negev, Israel)

Publisher's Version

Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(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 Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North
(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 Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert
(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, Emily Riehl, and Jonathan Weinberger
(Innopolis University, Russia; Johns Hopkins University, USA)

Publisher's Version Published Artifact Info Artifacts Available

proc time: 4.95