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 Article: poplws24cppmain-key1-p doi:10.1145/3636501.3637683

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 Article: poplws24cppmain-p47-p doi:10.1145/3636501.3636958

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

Publisher's Version Article: poplws24cppmain-p38-p doi:10.1145/3636501.3636953

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 Published Artifact Artifacts Available Article: poplws24cppmain-p4-p doi:10.1145/3636501.3636961

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 Article: poplws24cppmain-p16-p doi:10.1145/3636501.3636944

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 Article: poplws24cppmain-p2-p doi:10.1145/3636501.3636940

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

Publisher's Version Article: poplws24cppmain-p34-p doi:10.1145/3636501.3636950

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 Article: poplws24cppmain-p40-p doi:10.1145/3636501.3636954

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

Publisher's Version Published Artifact Artifacts Available Article: poplws24cppmain-p37-p doi:10.1145/3636501.3636952

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 Article: poplws24cppmain-p61-p doi:10.1145/3636501.3636959

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 Article: poplws24cppmain-p21-p doi:10.1145/3636501.3636946

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 Article: poplws24cppmain-p32-p doi:10.1145/3636501.3636949

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 Article: poplws24cppmain-p14-p doi:10.1145/3636501.3636943

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 Article: poplws24cppmain-p23-p doi:10.1145/3636501.3636947

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 Article: poplws24cppmain-p13-p doi:10.1145/3636501.3636942

Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Joseph Eremondi
(University of Edinburgh, UK)

Publisher's Version Info Article: poplws24cppmain-p26-p doi:10.1145/3636501.3636948

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 Article: poplws24cppmain-p45-p doi:10.1145/3636501.3636957

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 Article: poplws24cppmain-p36-p doi:10.1145/3636501.3636951

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 Article: poplws24cppmain-p43-p doi:10.1145/3636501.3636955

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 Article: poplws24cppmain-p44-p doi:10.1145/3636501.3636956

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 Article: poplws24cppmain-p18-p doi:10.1145/3636501.3636945

proc time: 0.04