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)


@InProceedings{CPP24p1, author = {Azalea Raad}, title = {Under-Approximation for Scalable Bug Detection (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3636501.3637683}, year = {2024}, } 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)


@InProceedings{CPP24p18, author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten}, title = {UTC Time, Formally Verified}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {18-17}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact 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)


@InProceedings{CPP24p35, author = {Andrew W. Appel and Ariel E. Kellison}, title = {VCFloat2: Floating-Point Error Analysis in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {35-34}, doi = {10.1145/3636501.3636953}, year = {2024}, } 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)


@InProceedings{CPP24p52, author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters}, title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {52-51}, doi = {10.1145/3636501.3636961}, year = {2024}, } 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)


@InProceedings{CPP24p69, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {69-68}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact 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)


@InProceedings{CPP24p86, author = {Duc-Than Nguyen and Lennart Beringer and William Mansky and Shengyi Wang}, title = {Compositional Verification of Concurrent C Programs with Search Structure Templates}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {86-85}, doi = {10.1145/3636501.3636940}, year = {2024}, } 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)


@InProceedings{CPP24p103, author = {Ike Mulder and Robbert Krebbers}, title = {Unification for Subformula Linking under Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {103-102}, doi = {10.1145/3636501.3636950}, year = {2024}, } 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)


@InProceedings{CPP24p120, author = {Clément Chavanon and Frédéric Besson and Tristan Ninet}, title = {PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {120-119}, doi = {10.1145/3636501.3636954}, year = {2024}, } 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)


@InProceedings{CPP24p137, author = {David Monniaux}, title = {Memory Simulations, Security and Optimization in a Verified Compiler}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {137-136}, doi = {10.1145/3636501.3636952}, year = {2024}, } 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)


@InProceedings{CPP24p154, author = {Ekaterina Zhuchko and Margus Veanes and Gabriel Ebner}, title = {Lean Formalization of Extended Regular Expression Matching with Lookarounds}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {154-153}, doi = {10.1145/3636501.3636959}, year = {2024}, } 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)


@InProceedings{CPP24p171, author = {Chelsea Edmonds and Lawrence C. Paulson}, title = {Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {171-170}, doi = {10.1145/3636501.3636946}, year = {2024}, } Publisher's Version 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)


@InProceedings{CPP24p188, author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann}, title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {188-187}, doi = {10.1145/3636501.3636949}, year = {2024}, } Publisher's Version 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)


@InProceedings{CPP24p205, author = {Lauren White and Laura Titolo and J. Tanner Slagel and César Muñoz}, title = {A Temporal Differential Dynamic Logic Formal Embedding}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {205-204}, doi = {10.1145/3636501.3636943}, year = {2024}, } 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)


@InProceedings{CPP24p222, author = {Siddhartha Gadgil and Anand Rao Tadipatri}, title = {Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {222-221}, doi = {10.1145/3636501.3636947}, year = {2024}, } 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)


@InProceedings{CPP24p239, author = {María Inés de Frutos-Fernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio}, title = {A Formalization of Complete Discrete Valuation Rings and Local Fields}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {239-238}, doi = {10.1145/3636501.3636942}, year = {2024}, } Publisher's Version 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)


@InProceedings{CPP24p256, author = {Joseph Eremondi}, title = {Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {256-255}, doi = {10.1145/3636501.3636948}, year = {2024}, } Publisher's Version 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)


@InProceedings{CPP24p273, author = {Ian Shillito and Dominik Kirst}, title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {273-272}, doi = {10.1145/3636501.3636957}, year = {2024}, } 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)


@InProceedings{CPP24p290, author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet}, title = {Martin-Löf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {290-289}, doi = {10.1145/3636501.3636951}, year = {2024}, } 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)


@InProceedings{CPP24p307, author = {Niels van der Weide and Nima Rasekh and Benedikt Ahrens and Paige Randall North}, title = {Univalent Double Categories}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {307-306}, doi = {10.1145/3636501.3636955}, year = {2024}, } 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)


@InProceedings{CPP24p324, author = {Benedikt Ahrens and Ralph Matthes and Niels van der Weide and Kobe Wullaert}, title = {Displayed Monoidal Categories for the Semantics of Linear Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {324-323}, doi = {10.1145/3636501.3636956}, year = {2024}, } 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)


@InProceedings{CPP24p341, author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger}, title = {Formalizing the ∞-Categorical Yoneda Lemma}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {341-340}, doi = {10.1145/3636501.3636945}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available Article: poplws24cppmain-p18-p doi:10.1145/3636501.3636945

proc time: 0.04