Workshop CPP 2024 – Author Index 
Contents 
Abstracts 
Authors

A B C D E G H J K L M N P R S T V W Z
Adjedj, Arthur 
CPP '24: "MartinLöf à la Coq ..."
MartinLöf à la Coq
Arthur Adjedj , Meven LennonBertrand , Kenji Maillard , PierreMarie Pédrot , and Loïc Pujet (ENS Paris Saclay  Université ParisSaclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden) We present an extensive mechanization of the metatheory of MartinLöf Type Theory (MLTT) in the Coq proof assistant. Our development builds on preexisting work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a fullfledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, inductionrecursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics. @InProceedings{CPP24p230, author = {Arthur Adjedj and Meven LennonBertrand and Kenji Maillard and PierreMarie Pédrot and Loïc Pujet}, title = {MartinLöf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {230245}, doi = {10.1145/3636501.3636951}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Ahrens, Benedikt 
CPP '24: "Univalent Double Categories ..."
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) Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities. @InProceedings{CPP24p246, 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 = {246259}, doi = {10.1145/3636501.3636955}, year = {2024}, } Publisher's Version CPP '24: "Displayed Monoidal Categories ..." 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) We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant. All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop "displayed monoidal categories". These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linearnonlinear categories and construct instances of them via Lafont categories and linear categories. @InProceedings{CPP24p260, 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 = {260273}, doi = {10.1145/3636501.3636956}, year = {2024}, } Publisher's Version 

Ang, Zhendong 
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic
Qiyuan Zhao , George Pîrlea , Zhendong Ang , Umang Mathur , and Ilya Sergey (National University of Singapore, Singapore) Arraybased encodings of tree structures are often preferable to linked or abstract data typebased representations for efficiency reasons. Compared to the more traditional encodings, arraybased trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals nonrecursively, requiring complex loop invariants for their correctness proofs. In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq. @InProceedings{CPP24p45, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4559}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Appel, Andrew W. 
CPP '24: "VCFloat2: FloatingPoint Error ..."
VCFloat2: FloatingPoint Error Analysis in Coq
Andrew W. Appel and Ariel E. Kellison (Princeton University, USA; Cornell University, USA) The development of sound and efficient tools that automatically perform floatingpoint roundoff error analysis is an active area of research with applications to embedded systems and scientific computing. In this paper we describe VCFloat2, a novel extension to the VCFloat tool for verifying floatingpoint C programs in Coq. Like VCFloat1, VCFloat2 soundly and automatically computes roundoff error bounds on floatingpoint expressions, but does so to higher accuracy; with better performance; with more generality for nonstandard number formats; with the ability to reason about external (userdefined or library) functions; and with improved modularity for interfacing with other program verification tools in Coq. We evaluate the performance of VCFloat2 using common benchmarks; compared to other stateofthe art tools, VCFloat2 computes competitive error bounds and transparent certificates that require less time for verification. @InProceedings{CPP24p14, author = {Andrew W. Appel and Ariel E. Kellison}, title = {VCFloat2: FloatingPoint Error Analysis in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1429}, doi = {10.1145/3636501.3636953}, year = {2024}, } Publisher's Version 

Beringer, Lennart 
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
DucThan Nguyen , Lennart Beringer , William Mansky , and Shengyi Wang (University of Illinois at Chicago, USA; Princeton University, USA) Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrencycontrol and datastructure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of finegrained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of realworld concurrent data structures. @InProceedings{CPP24p60, author = {DucThan 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 = {6074}, doi = {10.1145/3636501.3636940}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Besson, Frédéric 
CPP '24: "PfComp: A Verified Compiler ..."
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) We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules. @InProceedings{CPP24p89, 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 = {89102}, doi = {10.1145/3636501.3636954}, year = {2024}, } Publisher's Version 

Casals Buñuel, Joaquim 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Chavanon, Clément 
CPP '24: "PfComp: A Verified Compiler ..."
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) We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules. @InProceedings{CPP24p89, 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 = {89102}, doi = {10.1145/3636501.3636954}, year = {2024}, } Publisher's Version 

Conejero Rodríguez, Juan 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

De Almeida Borges, Ana 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

De FrutosFernández, María Inés 
CPP '24: "A Formalization of Complete ..."
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de FrutosFernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio (Autonomous University of Madrid, Spain; Université Jean Monnet SaintÉtienne, France) Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some localization results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field ℚ_{p} of padic numbers and of the field F_{p}((X)) of Laurent series over F_{p} are local fields. @InProceedings{CPP24p190, author = {María Inés de FrutosFerná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 = {190204}, doi = {10.1145/3636501.3636942}, year = {2024}, } Publisher's Version Info 

Ebner, Gabriel 
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko , Margus Veanes , and Gabriel Ebner (Tallinn University of Technology, Estonia; Microsoft Research, USA) We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant. The proof of its correctness is with respect to standard matching semantics. @InProceedings{CPP24p118, 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 = {118131}, doi = {10.1145/3636501.3636959}, year = {2024}, } Publisher's Version 

Edmonds, Chelsea 
CPP '24: "Formal Probabilistic Methods ..."
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) Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? We present a modular framework using locales in Isabelle/HOL to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lovász local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, and highlights several notable gaps in typical intuitive probabilistic reasoning on paper. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings. @InProceedings{CPP24p132, 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 = {132146}, doi = {10.1145/3636501.3636946}, year = {2024}, } Publisher's Version Info 

Eremondi, Joseph 
CPP '24: "Strictly Monotone Brouwer ..."
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Joseph Eremondi (University of Edinburgh, UK) Ordinals can be used to prove the termination of dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend unary natural numbers with a limit constructor, so a function's size can be the least upper bound of the sizes of values from its image. These can then be used to define wellfounded recursion: any recursive calls are allowed so long as they are on values whose sizes are strictly smaller than the current size. Unfortunately, Brouwer trees are not algebraically wellbehaved. They can be characterized equationally as a joinsemilattice, where the join takes the maximum of two trees. However, this join does not interact well with the successor constructor, so it does not interact properly with the strict ordering used in wellfounded recursion. We present Strictly Monotone Brouwer trees (SMBtrees), a refinement of Brouwer trees that are algebraically wellbehaved. SMBtrees are built using functions with the same signatures as Brouwer tree constructors, and they satisfy all Brouwer tree inequalities. However, their join operator distributes over the successor, making them suited for wellfounded recursion or equational reasoning. This paper teaches how, using dependent pairs and careful definitions, an illbehaved definition can be turned into a wellbehaved one. Our approach is axiomatically lightweight: it does not rely on Axiom K, univalence, quotient types, or Higher Inductive Types. We implement a recursivelydefined maximum operator for Brouwer trees that matches on successors and handles them specifically. Then, we define SMBtrees as the subset of Brouwer trees for which the recursive maximum computes a least upper bound. Finally, we show that every Brouwer tree can be transformed into a corresponding SMBtree by infinitely joining it with itself. All definitions and theorems are implemented in Agda. @InProceedings{CPP24p205, author = {Joseph Eremondi}, title = {Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {205217}, doi = {10.1145/3636501.3636948}, year = {2024}, } Publisher's Version Info 

Gadgil, Siddhartha 
CPP '24: "Formalizing Giles Gardam’s ..."
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) We describe a formalization in Lean 4 of Giles Gardam's disproof of Kaplansky's Unit Conjecture. This makes use of a combination of deductive proving and formally verified computation, using the nature of Lean 4 as a programming language which is also a proof assistant. Our goal in this work, besides formalization of the specific result, is to show what is possible with the current state of the art and illustrate how it can be achieved. Specifically we illustrate real time formalization of an important mathematical result and the seamless integration of proofs and computations in Lean 4. @InProceedings{CPP24p177, author = {Siddhartha Gadgil and Anand Rao Tadipatri}, title = {Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {177189}, doi = {10.1145/3636501.3636947}, year = {2024}, } Publisher's Version 

González Bedmar, Mireia 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Hansen, Lasse Letager 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Haselwarter, Philipp G. 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Hermo Reyes, Eduardo 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Hirokawa, Nao 
CPP '24: "Certification of Confluence ..."
Certification of Confluence and CommutationProofs via Parallel Critical Pairs
Nao Hirokawa , Dohan Kim , Kiraku Shintani , and René Thiemann (JAIST, Japan; University of Innsbruck, Austria) Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paperdefinition of PCPs, i.e., we switch from a positionbased definition to a contextbased definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence and commutationproofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known. @InProceedings{CPP24p147, author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann}, title = {Certification of Confluence and CommutationProofs via Parallel Critical Pairs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {147161}, doi = {10.1145/3636501.3636949}, year = {2024}, } Publisher's Version Info 

Hriţcu, Cătălin 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Hvass, Benjamin Salling 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Joosten, Joost J. 
CPP '24: "UTC Time, Formally Verified ..."
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) FV Time is a smallscale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet nontrivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some generalpurpose solutions that were produced as byproducts and may be used in other verification projects. These include a refinement package between prooforiented MathComp numbers and computationoriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through bruteforce computation. @InProceedings{CPP24p2, 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 = {213}, doi = {10.1145/3636501.3636958}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Kellison, Ariel E. 
CPP '24: "VCFloat2: FloatingPoint Error ..."
VCFloat2: FloatingPoint Error Analysis in Coq
Andrew W. Appel and Ariel E. Kellison (Princeton University, USA; Cornell University, USA) The development of sound and efficient tools that automatically perform floatingpoint roundoff error analysis is an active area of research with applications to embedded systems and scientific computing. In this paper we describe VCFloat2, a novel extension to the VCFloat tool for verifying floatingpoint C programs in Coq. Like VCFloat1, VCFloat2 soundly and automatically computes roundoff error bounds on floatingpoint expressions, but does so to higher accuracy; with better performance; with more generality for nonstandard number formats; with the ability to reason about external (userdefined or library) functions; and with improved modularity for interfacing with other program verification tools in Coq. We evaluate the performance of VCFloat2 using common benchmarks; compared to other stateofthe art tools, VCFloat2 computes competitive error bounds and transparent certificates that require less time for verification. @InProceedings{CPP24p14, author = {Andrew W. Appel and Ariel E. Kellison}, title = {VCFloat2: FloatingPoint Error Analysis in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1429}, doi = {10.1145/3636501.3636953}, year = {2024}, } Publisher's Version 

Kim, Dohan 
CPP '24: "Certification of Confluence ..."
Certification of Confluence and CommutationProofs via Parallel Critical Pairs
Nao Hirokawa , Dohan Kim , Kiraku Shintani , and René Thiemann (JAIST, Japan; University of Innsbruck, Austria) Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paperdefinition of PCPs, i.e., we switch from a positionbased definition to a contextbased definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence and commutationproofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known. @InProceedings{CPP24p147, author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann}, title = {Certification of Confluence and CommutationProofs via Parallel Critical Pairs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {147161}, doi = {10.1145/3636501.3636949}, year = {2024}, } Publisher's Version Info 

Kirst, Dominik 
CPP '24: "A Mechanised and Constructive ..."
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Biintuitionistic Logic
Ian Shillito and Dominik Kirst (Australian National University, Australia; BenGurion University of the Negev, Israel) Using the Coq proof assistant, we investigate the minimal nonconstructive principles needed to show soundness and completeness of propositional biintuitionistic logic. Before being revisited and corrected by Goré and Shillito, the completeness of biintuitionistic logic, an extension of intuitionistic logic with a dual operation to implication, had a rather erratic history, making it an ideal case for computer mechanisation. Moreover, contributing a constructive perspective, we observe that the completeness of biintuitionistic logic explicates the same characteristics already observed in an ongoing effort to analyse completeness theorems in general. @InProceedings{CPP24p218, author = {Ian Shillito and Dominik Kirst}, title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Biintuitionistic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {218229}, doi = {10.1145/3636501.3636957}, year = {2024}, } Publisher's Version 

Krebbers, Robbert 
CPP '24: "Unification for Subformula ..."
Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers (Radboud University Nijmegen, Netherlands) Subformula linking is a technique that allows one to simplify proof goals by identifying subformulas of hypotheses that share atoms with the goal. It has been used by recent prototypes for gesturebased interactive theorem proving, but also for theorem proving in separation logic. When linking formulas, we should avoid information loss, i.e., subformula linking should succeed precisely when a provable simplification can be generated. Avoiding information loss is challenging when quantifiers are involved. Existing approaches either generate simplifications that involve equalities, or determine substitutions for variables via unification. The first approach can produce unprovable simplifications, while the second approach can fail to find desired links. We propose a third approach, called Quantifying on the Uninstantiated (QU), which is also based on unification and lies between the two existing approaches. We show that QU has practical applications for proof automation, by improving tactics for resource framing in the Iris framework for separation logic in Coq. @InProceedings{CPP24p75, author = {Ike Mulder and Robbert Krebbers}, title = {Unification for Subformula Linking under Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7588}, doi = {10.1145/3636501.3636950}, year = {2024}, } Publisher's Version 

Kudasov, Nikolai 
CPP '24: "Formalizing the ∞Categorical ..."
Formalizing the ∞Categorical Yoneda Lemma
Nikolai Kudasov , Emily Riehl , and Jonathan Weinberger (Innopolis University, Russia; Johns Hopkins University, USA) Formalized 1category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinitedimensional categories in place of 1dimensional categories, and ∞category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl–Shulman’s simplicial extension of homotopy type theory for synthetic ∞category theory, we provide the first formalizations of results from ∞category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from ∞category theory, such as the theory of limits and colimits and adjunctions. @InProceedings{CPP24p274, author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger}, title = {Formalizing the ∞Categorical Yoneda Lemma}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {274290}, doi = {10.1145/3636501.3636945}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

LennonBertrand, Meven 
CPP '24: "MartinLöf à la Coq ..."
MartinLöf à la Coq
Arthur Adjedj , Meven LennonBertrand , Kenji Maillard , PierreMarie Pédrot , and Loïc Pujet (ENS Paris Saclay  Université ParisSaclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden) We present an extensive mechanization of the metatheory of MartinLöf Type Theory (MLTT) in the Coq proof assistant. Our development builds on preexisting work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a fullfledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, inductionrecursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics. @InProceedings{CPP24p230, author = {Arthur Adjedj and Meven LennonBertrand and Kenji Maillard and PierreMarie Pédrot and Loïc Pujet}, title = {MartinLöf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {230245}, doi = {10.1145/3636501.3636951}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Maillard, Kenji 
CPP '24: "MartinLöf à la Coq ..."
MartinLöf à la Coq
Arthur Adjedj , Meven LennonBertrand , Kenji Maillard , PierreMarie Pédrot , and Loïc Pujet (ENS Paris Saclay  Université ParisSaclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden) We present an extensive mechanization of the metatheory of MartinLöf Type Theory (MLTT) in the Coq proof assistant. Our development builds on preexisting work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a fullfledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, inductionrecursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics. @InProceedings{CPP24p230, author = {Arthur Adjedj and Meven LennonBertrand and Kenji Maillard and PierreMarie Pédrot and Loïc Pujet}, title = {MartinLöf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {230245}, doi = {10.1145/3636501.3636951}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Mansky, William 
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
DucThan Nguyen , Lennart Beringer , William Mansky , and Shengyi Wang (University of Illinois at Chicago, USA; Princeton University, USA) Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrencycontrol and datastructure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of finegrained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of realworld concurrent data structures. @InProceedings{CPP24p60, author = {DucThan 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 = {6074}, doi = {10.1145/3636501.3636940}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Mathur, Umang 
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic
Qiyuan Zhao , George Pîrlea , Zhendong Ang , Umang Mathur , and Ilya Sergey (National University of Singapore, Singapore) Arraybased encodings of tree structures are often preferable to linked or abstract data typebased representations for efficiency reasons. Compared to the more traditional encodings, arraybased trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals nonrecursively, requiring complex loop invariants for their correctness proofs. In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq. @InProceedings{CPP24p45, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4559}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Matthes, Ralph 
CPP '24: "Displayed Monoidal Categories ..."
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) We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant. All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop "displayed monoidal categories". These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linearnonlinear categories and construct instances of them via Lafont categories and linear categories. @InProceedings{CPP24p260, 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 = {260273}, doi = {10.1145/3636501.3636956}, year = {2024}, } Publisher's Version 

Monniaux, David 
CPP '24: "Memory Simulations, Security ..."
Memory Simulations, Security and Optimization in a Verified Compiler
David Monniaux (University of Grenoble Alpes  CNRS  Grenoble INP  VERIMAG, France) Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined values, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler. @InProceedings{CPP24p103, author = {David Monniaux}, title = {Memory Simulations, Security and Optimization in a Verified Compiler}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {103117}, doi = {10.1145/3636501.3636952}, year = {2024}, } Publisher's Version 

Mulder, Ike 
CPP '24: "Unification for Subformula ..."
Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers (Radboud University Nijmegen, Netherlands) Subformula linking is a technique that allows one to simplify proof goals by identifying subformulas of hypotheses that share atoms with the goal. It has been used by recent prototypes for gesturebased interactive theorem proving, but also for theorem proving in separation logic. When linking formulas, we should avoid information loss, i.e., subformula linking should succeed precisely when a provable simplification can be generated. Avoiding information loss is challenging when quantifiers are involved. Existing approaches either generate simplifications that involve equalities, or determine substitutions for variables via unification. The first approach can produce unprovable simplifications, while the second approach can fail to find desired links. We propose a third approach, called Quantifying on the Uninstantiated (QU), which is also based on unification and lies between the two existing approaches. We show that QU has practical applications for proof automation, by improving tactics for resource framing in the Iris framework for separation logic in Coq. @InProceedings{CPP24p75, author = {Ike Mulder and Robbert Krebbers}, title = {Unification for Subformula Linking under Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7588}, doi = {10.1145/3636501.3636950}, year = {2024}, } Publisher's Version 

Muñoz, César 
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White , Laura Titolo , J. Tanner Slagel , and César Muñoz (NASA, USA; AMA, USA) Differential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL2 in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL, which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies. @InProceedings{CPP24p162, 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 = {162176}, doi = {10.1145/3636501.3636943}, year = {2024}, } Publisher's Version 

Nguyen, DucThan 
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
DucThan Nguyen , Lennart Beringer , William Mansky , and Shengyi Wang (University of Illinois at Chicago, USA; Princeton University, USA) Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrencycontrol and datastructure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of finegrained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of realworld concurrent data structures. @InProceedings{CPP24p60, author = {DucThan 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 = {6074}, doi = {10.1145/3636501.3636940}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Ninet, Tristan 
CPP '24: "PfComp: A Verified Compiler ..."
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) We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules. @InProceedings{CPP24p89, 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 = {89102}, doi = {10.1145/3636501.3636954}, year = {2024}, } Publisher's Version 

North, Paige Randall 
CPP '24: "Univalent Double Categories ..."
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) Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities. @InProceedings{CPP24p246, 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 = {246259}, doi = {10.1145/3636501.3636955}, year = {2024}, } Publisher's Version 

Nuccio Mortarino Majno di Capriglio, Filippo Alberto Edoardo 
CPP '24: "A Formalization of Complete ..."
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de FrutosFernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio (Autonomous University of Madrid, Spain; Université Jean Monnet SaintÉtienne, France) Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some localization results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field ℚ_{p} of padic numbers and of the field F_{p}((X)) of Laurent series over F_{p} are local fields. @InProceedings{CPP24p190, author = {María Inés de FrutosFerná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 = {190204}, doi = {10.1145/3636501.3636942}, year = {2024}, } Publisher's Version Info 

Paulson, Lawrence C. 
CPP '24: "Formal Probabilistic Methods ..."
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) Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? We present a modular framework using locales in Isabelle/HOL to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lovász local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, and highlights several notable gaps in typical intuitive probabilistic reasoning on paper. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings. @InProceedings{CPP24p132, 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 = {132146}, doi = {10.1145/3636501.3636946}, year = {2024}, } Publisher's Version Info 

Pédrot, PierreMarie 
CPP '24: "MartinLöf à la Coq ..."
MartinLöf à la Coq
Arthur Adjedj , Meven LennonBertrand , Kenji Maillard , PierreMarie Pédrot , and Loïc Pujet (ENS Paris Saclay  Université ParisSaclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden) We present an extensive mechanization of the metatheory of MartinLöf Type Theory (MLTT) in the Coq proof assistant. Our development builds on preexisting work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a fullfledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, inductionrecursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics. @InProceedings{CPP24p230, author = {Arthur Adjedj and Meven LennonBertrand and Kenji Maillard and PierreMarie Pédrot and Loïc Pujet}, title = {MartinLöf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {230245}, doi = {10.1145/3636501.3636951}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Pîrlea, George 
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic
Qiyuan Zhao , George Pîrlea , Zhendong Ang , Umang Mathur , and Ilya Sergey (National University of Singapore, Singapore) Arraybased encodings of tree structures are often preferable to linked or abstract data typebased representations for efficiency reasons. Compared to the more traditional encodings, arraybased trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals nonrecursively, requiring complex loop invariants for their correctness proofs. In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq. @InProceedings{CPP24p45, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4559}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Pujet, Loïc 
CPP '24: "MartinLöf à la Coq ..."
MartinLöf à la Coq
Arthur Adjedj , Meven LennonBertrand , Kenji Maillard , PierreMarie Pédrot , and Loïc Pujet (ENS Paris Saclay  Université ParisSaclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden) We present an extensive mechanization of the metatheory of MartinLöf Type Theory (MLTT) in the Coq proof assistant. Our development builds on preexisting work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a fullfledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, inductionrecursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics. @InProceedings{CPP24p230, author = {Arthur Adjedj and Meven LennonBertrand and Kenji Maillard and PierreMarie Pédrot and Loïc Pujet}, title = {MartinLöf à la Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {230245}, doi = {10.1145/3636501.3636951}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Raad, Azalea 
CPP '24: "UnderApproximation for Scalable ..."
UnderApproximation for Scalable Bug Detection (Keynote)
Azalea Raad (Imperial College London, UK) Incorrectness Logic (IL) has recently been advanced as a logical underapproximate theory for proving the presence of bugs  dual to Hoare Logic, which is an overapproximate theory for proving the absence of bugs. To facilitate scalable bug detection, later we developed incorrectness separation logic (ISL) by marrying the underapproximate reasoning of IL with the local reasoning of separation logic and its frame rule. This locality leads to techniques that are compositional both in code (concentrating on a program component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a component sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. We then developed PulseX, an automatic program analysis for catching memory safety errors, underpinned by ISL. Using PulseX, deployed at Meta, we found a number of real bugs in codebases such as OpenSSL, which were subsequently confirmed and fixed. We have compared the performance of PulseX against the stateoftheart tool Infer on a number of large programs; our comparison shows that PulseX is comparable with Infer in terms of performance, and in certain cases its fixrate surpasses that of Infer. @InProceedings{CPP24p1, author = {Azalea Raad}, title = {UnderApproximation for Scalable Bug Detection (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {11}, doi = {10.1145/3636501.3637683}, year = {2024}, } Publisher's Version 

Rasekh, Nima 
CPP '24: "Univalent Double Categories ..."
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) Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities. @InProceedings{CPP24p246, 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 = {246259}, doi = {10.1145/3636501.3636955}, year = {2024}, } Publisher's Version 

Riehl, Emily 
CPP '24: "Formalizing the ∞Categorical ..."
Formalizing the ∞Categorical Yoneda Lemma
Nikolai Kudasov , Emily Riehl , and Jonathan Weinberger (Innopolis University, Russia; Johns Hopkins University, USA) Formalized 1category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinitedimensional categories in place of 1dimensional categories, and ∞category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl–Shulman’s simplicial extension of homotopy type theory for synthetic ∞category theory, we provide the first formalizations of results from ∞category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from ∞category theory, such as the theory of limits and colimits and adjunctions. @InProceedings{CPP24p274, author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger}, title = {Formalizing the ∞Categorical Yoneda Lemma}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {274290}, doi = {10.1145/3636501.3636945}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Sergey, Ilya 
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic
Qiyuan Zhao , George Pîrlea , Zhendong Ang , Umang Mathur , and Ilya Sergey (National University of Singapore, Singapore) Arraybased encodings of tree structures are often preferable to linked or abstract data typebased representations for efficiency reasons. Compared to the more traditional encodings, arraybased trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals nonrecursively, requiring complex loop invariants for their correctness proofs. In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq. @InProceedings{CPP24p45, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4559}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Shillito, Ian 
CPP '24: "A Mechanised and Constructive ..."
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Biintuitionistic Logic
Ian Shillito and Dominik Kirst (Australian National University, Australia; BenGurion University of the Negev, Israel) Using the Coq proof assistant, we investigate the minimal nonconstructive principles needed to show soundness and completeness of propositional biintuitionistic logic. Before being revisited and corrected by Goré and Shillito, the completeness of biintuitionistic logic, an extension of intuitionistic logic with a dual operation to implication, had a rather erratic history, making it an ideal case for computer mechanisation. Moreover, contributing a constructive perspective, we observe that the completeness of biintuitionistic logic explicates the same characteristics already observed in an ongoing effort to analyse completeness theorems in general. @InProceedings{CPP24p218, author = {Ian Shillito and Dominik Kirst}, title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Biintuitionistic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {218229}, doi = {10.1145/3636501.3636957}, year = {2024}, } Publisher's Version 

Shintani, Kiraku 
CPP '24: "Certification of Confluence ..."
Certification of Confluence and CommutationProofs via Parallel Critical Pairs
Nao Hirokawa , Dohan Kim , Kiraku Shintani , and René Thiemann (JAIST, Japan; University of Innsbruck, Austria) Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paperdefinition of PCPs, i.e., we switch from a positionbased definition to a contextbased definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence and commutationproofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known. @InProceedings{CPP24p147, author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann}, title = {Certification of Confluence and CommutationProofs via Parallel Critical Pairs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {147161}, doi = {10.1145/3636501.3636949}, year = {2024}, } Publisher's Version Info 

Slagel, J. Tanner 
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White , Laura Titolo , J. Tanner Slagel , and César Muñoz (NASA, USA; AMA, USA) Differential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL2 in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL, which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies. @InProceedings{CPP24p162, 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 = {162176}, doi = {10.1145/3636501.3636943}, year = {2024}, } Publisher's Version 

Spitters, Bas 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Tadipatri, Anand Rao 
CPP '24: "Formalizing Giles Gardam’s ..."
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) We describe a formalization in Lean 4 of Giles Gardam's disproof of Kaplansky's Unit Conjecture. This makes use of a combination of deductive proving and formally verified computation, using the nature of Lean 4 as a programming language which is also a proof assistant. Our goal in this work, besides formalization of the specific result, is to show what is possible with the current state of the art and illustrate how it can be achieved. Specifically we illustrate real time formalization of an important mathematical result and the seamless integration of proofs and computations in Lean 4. @InProceedings{CPP24p177, author = {Siddhartha Gadgil and Anand Rao Tadipatri}, title = {Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {177189}, doi = {10.1145/3636501.3636947}, year = {2024}, } Publisher's Version 

Thiemann, René 
CPP '24: "Certification of Confluence ..."
Certification of Confluence and CommutationProofs via Parallel Critical Pairs
Nao Hirokawa , Dohan Kim , Kiraku Shintani , and René Thiemann (JAIST, Japan; University of Innsbruck, Austria) Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paperdefinition of PCPs, i.e., we switch from a positionbased definition to a contextbased definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence and commutationproofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known. @InProceedings{CPP24p147, author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann}, title = {Certification of Confluence and CommutationProofs via Parallel Critical Pairs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {147161}, doi = {10.1145/3636501.3636949}, year = {2024}, } Publisher's Version Info 

Titolo, Laura 
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White , Laura Titolo , J. Tanner Slagel , and César Muñoz (NASA, USA; AMA, USA) Differential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL2 in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL, which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies. @InProceedings{CPP24p162, 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 = {162176}, doi = {10.1145/3636501.3636943}, year = {2024}, } Publisher's Version 

Van der Weide, Niels 
CPP '24: "Univalent Double Categories ..."
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) Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities. @InProceedings{CPP24p246, 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 = {246259}, doi = {10.1145/3636501.3636955}, year = {2024}, } Publisher's Version CPP '24: "Displayed Monoidal Categories ..." 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) We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant. All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop "displayed monoidal categories". These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linearnonlinear categories and construct instances of them via Lafont categories and linear categories. @InProceedings{CPP24p260, 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 = {260273}, doi = {10.1145/3636501.3636956}, year = {2024}, } Publisher's Version 

Veanes, Margus 
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko , Margus Veanes , and Gabriel Ebner (Tallinn University of Technology, Estonia; Microsoft Research, USA) We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant. The proof of its correctness is with respect to standard matching semantics. @InProceedings{CPP24p118, 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 = {118131}, doi = {10.1145/3636501.3636959}, year = {2024}, } Publisher's Version 

Wang, Shengyi 
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
DucThan Nguyen , Lennart Beringer , William Mansky , and Shengyi Wang (University of Illinois at Chicago, USA; Princeton University, USA) Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrencycontrol and datastructure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of finegrained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of realworld concurrent data structures. @InProceedings{CPP24p60, author = {DucThan 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 = {6074}, doi = {10.1145/3636501.3636940}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available 

Weinberger, Jonathan 
CPP '24: "Formalizing the ∞Categorical ..."
Formalizing the ∞Categorical Yoneda Lemma
Nikolai Kudasov , Emily Riehl , and Jonathan Weinberger (Innopolis University, Russia; Johns Hopkins University, USA) Formalized 1category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinitedimensional categories in place of 1dimensional categories, and ∞category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl–Shulman’s simplicial extension of homotopy type theory for synthetic ∞category theory, we provide the first formalizations of results from ∞category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from ∞category theory, such as the theory of limits and colimits and adjunctions. @InProceedings{CPP24p274, author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger}, title = {Formalizing the ∞Categorical Yoneda Lemma}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {274290}, doi = {10.1145/3636501.3636945}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

White, Lauren 
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White , Laura Titolo , J. Tanner Slagel , and César Muñoz (NASA, USA; AMA, USA) Differential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL2 in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL, which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies. @InProceedings{CPP24p162, 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 = {162176}, doi = {10.1145/3636501.3636943}, year = {2024}, } Publisher's Version 

Winterhalter, Théo 
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational EndtoEnd Verification of HighSpeed 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; MPISP, Germany) The field of highassurance cryptography is quickly maturing, yet a unified foundational framework for endtoend formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, highassurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational endtoend Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES. @InProceedings{CPP24p30, 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 EndtoEnd Verification of HighSpeed Cryptography}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3044}, doi = {10.1145/3636501.3636961}, year = {2024}, } Publisher's Version 

Wullaert, Kobe 
CPP '24: "Displayed Monoidal Categories ..."
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) We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant. All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop "displayed monoidal categories". These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linearnonlinear categories and construct instances of them via Lafont categories and linear categories. @InProceedings{CPP24p260, 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 = {260273}, doi = {10.1145/3636501.3636956}, year = {2024}, } Publisher's Version 

Zhao, Qiyuan 
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic
Qiyuan Zhao , George Pîrlea , Zhendong Ang , Umang Mathur , and Ilya Sergey (National University of Singapore, Singapore) Arraybased encodings of tree structures are often preferable to linked or abstract data typebased representations for efficiency reasons. Compared to the more traditional encodings, arraybased trees do not immediately offer convenient induction principles, and the programs that manipulate them often implement traversals nonrecursively, requiring complex loop invariants for their correctness proofs. In this work, we provide a set of definitions, lemmas, and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase our proof techniques via a series of small but characteristic examples, culminating with a large case study: verification of a C implementation of a recently published tree clock data structure in a Separation Logic embedded into Coq. @InProceedings{CPP24p45, author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey}, title = {Rooting for Efficiency: Mechanised Reasoning about ArrayBased Trees in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4559}, doi = {10.1145/3636501.3636944}, year = {2024}, } Publisher's Version Published Artifact Info Artifacts Available 

Zhuchko, Ekaterina 
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko , Margus Veanes , and Gabriel Ebner (Tallinn University of Technology, Estonia; Microsoft Research, USA) We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant. The proof of its correctness is with respect to standard matching semantics. @InProceedings{CPP24p118, 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 = {118131}, doi = {10.1145/3636501.3636959}, year = {2024}, } Publisher's Version 
64 authors
proc time: 16.62