Workshop CPP 2023 – Author Index 
Contents 
Abstracts 
Authors

A B C D E F G H I J K L M N P R S T U V W Y
Affeldt, Reynald 
CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using sFinite Kernels in Coq
Reynald Affeldt , Cyril Cohen , and Ayumu Saito (AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan) Probabilistic programming languages are used to write probabilistic models to make probabilistic inferences. A number of rigorous semantics have recently been proposed that are now available to carry out formal verification of probabilistic programs. In this paper, we extend an existing formalization of measure and integration theory with sfinite kernels, a mathematical structure to interpret typing judgments in the semantics of a probabilistic programming language. The resulting library makes it possible to reason formally about transformations of probabilistic programs and their execution. @InProceedings{CPP23p3, author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito}, title = {Semantics of Probabilistic Programs using sFinite Kernels in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {316}, doi = {10.1145/3573105.3575691}, year = {2023}, } Publisher's Version 

Allamigeon, Xavier 
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon , Quentin Canu , and PierreYves Strub (Inria, France; École Polytechnique, France; Meta, France) The purpose of this paper is the formal verification of a counterexample of Santos et al. to the socalled Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the penandpaper proof, our approach is entirely computational: we have implemented in Coq and proved correct an algorithm that explicitly computes, within the proof assistant, vertexedge graphs of polytopes as well as their diameter. The originality of this certificatebased algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over prooforiented data types and the correspondence with a lowlevel implementation over computationoriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g. matrix multiplications, basic routines on graphs), in order to make the derivation of the correctness of the lowlevel implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples to Hirsch conjecture due to Matschke, Santos and Weibel, respectively 20 and 23dimensional polytopes with 36425 and 73224 vertices involving rational coefficients with up to 20 digits. We also illustrate the performance of the method by computing the list of vertices or the diameter of wellknown classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem. @InProceedings{CPP23p17, author = {Xavier Allamigeon and Quentin Canu and PierreYves Strub}, title = {A Formal Disproof of Hirsch Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1729}, doi = {10.1145/3573105.3575678}, year = {2023}, } Publisher's Version 

Annenkov, Danil 
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen , Danil Annenkov , and Bas Spitters (Aarhus University, Denmark) The number of attacks and accidents leading to significant losses of cryptoassets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, noncustodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter’s implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns. @InProceedings{CPP23p290, author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters}, title = {Formalising Decentralised Exchanges in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {290302}, doi = {10.1145/3573105.3575685}, year = {2023}, } Publisher's Version 

Arasu, Arvind 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Arnaboldi, Luca 
CPP '23: "Compiling HigherOrder Specifications ..."
Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt , Robert Atkey , Wen Kokke , Ekaterina Komendantskaya , and Luca Arnaboldi (HeriotWatt University, UK; University of Strathclyde, UK; University of Edinburgh, UK) Modern verification tools frequently rely on compiling highlevel specifications to SMT queries. However, the highlevel specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unificationbased typechecker with type classes and automatic generalisation. Concretely, typechecking is used as a constructive procedure for underapproximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda. @InProceedings{CPP23p102, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102120}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version Info 

Ataei, Parisa 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Atkey, Robert 
CPP '23: "Compiling HigherOrder Specifications ..."
Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt , Robert Atkey , Wen Kokke , Ekaterina Komendantskaya , and Luca Arnaboldi (HeriotWatt University, UK; University of Strathclyde, UK; University of Edinburgh, UK) Modern verification tools frequently rely on compiling highlevel specifications to SMT queries. However, the highlevel specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unificationbased typechecker with type classes and automatic generalisation. Concretely, typechecking is used as a constructive procedure for underapproximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda. @InProceedings{CPP23p102, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102120}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version Info 

Baanen, Anne 
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen , Alex J. Best , Nirvana Coppola , and Sander R. Dahmen (Vrije Universiteit Amsterdam, Netherlands) Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y^{2}=x^{3}+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One nonelementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond. @InProceedings{CPP23p47, author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen}, title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4762}, doi = {10.1145/3573105.3575682}, year = {2023}, } Publisher's Version Info 

Bakšys, Mantas 
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki KoutsoukouArgyraki , Mantas Bakšys , and Chelsea Edmonds (University of Cambridge, UK) We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers’s proof deriving the first effective bounds for Szemerédi’s Theorem. The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects. This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging. We demonstrate how locales, Isabelle’s module system, can be employed to handle such interplays in mathematical formalisations. To treat the graphtheoretic aspects of the proof, we make use of a new, more general undirected graph theory library developed by Edmonds, which is both flexible and extensible. In addition to the main theorem, which, following our source, is formulated for difference sets, we also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality. We moreover formalise a few additional results in additive combinatorics that are not used in the proof of the main theorem. This is the first formalisation of the Balog–Szemerédi–Gowers Theorem in any proof assistant to our knowledge. @InProceedings{CPP23p225, author = {Angeliki KoutsoukouArgyraki and Mantas Bakšys and Chelsea Edmonds}, title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {225238}, doi = {10.1145/3573105.3575680}, year = {2023}, } Publisher's Version 

Best, Alex J. 
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen , Alex J. Best , Nirvana Coppola , and Sander R. Dahmen (Vrije Universiteit Amsterdam, Netherlands) Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y^{2}=x^{3}+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One nonelementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond. @InProceedings{CPP23p47, author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen}, title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4762}, doi = {10.1145/3573105.3575682}, year = {2023}, } Publisher's Version Info 

Blazy, Sandrine 
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz , Delphine Demange , and Sandrine Blazy (Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France) The Gated Static Single Assignment (GSA) form was proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analyses and optimisation passes in compilers. Compared to SSA, GSA records additional data dependencies and provides more context, making optimisations more effective and allowing one to reason about programs as dataflow graphs. Many practical implementations have been proposed that follow, more or less faithfully, Ottenstein et al.'s seminal paper. But many discrepancies remain between these, depending on the kind of dependencies they are supposed to track and to leverage in analyses and code optimisations. In this paper, we present a formal semantics for GSA, mechanised in Coq. In particular, we clarify the nature and the purpose of gates in GSA, and define controlflow insensitive semantics for them. We provide a specification that can be used as a reference description for GSA. We also specify a translation from SSA to GSA and prove that this specification is semanticspreserving. We demonstrate that the approach is practical by implementing the specification as a validated translation within the CompCertSSA verified compiler. @InProceedings{CPP23p182, author = {Yann Herklotz and Delphine Demange and Sandrine Blazy}, title = {Mechanised Semantics for Gated Static Single Assignment}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {182196}, doi = {10.1145/3573105.3575681}, year = {2023}, } Publisher's Version CPP '23: "CompCert: A Journey through ..." CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote) Sandrine Blazy (University of Rennes, France; Inria, France; CNRS, France; IRISA, France) A formally verified compiler ensures that compilation does not introduce any bugs in programs. In the CompCert C compiler, this correctness property requires reasoning about realistic languages by using a semantic framework. This invited talk explains how this framework has been effectively used to turn CompCert from a prototype in a lab into a realworld compiler. @InProceedings{CPP23p1, author = {Sandrine Blazy}, title = {CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {11}, doi = {10.1145/3573105.3579107}, year = {2023}, } Publisher's Version 

Blot, Valentin 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Bordg, Anthony 
CPP '23: "Encoding DependentlyTyped ..."
Encoding DependentlyTyped Constructions into Simple Type Theory
Anthony Bordg and Adrián Doña Mateo (University of Cambridge, UK; University of Edinburgh, UK) In this article, we show how one can formalise in type theory mathematical objects, for which dependent types are usually deemed unavoidable, using only simple types. We outline a method to encode most of the terms of Lean's dependent type theory into the simple type theory of Isabelle/HOL. Taking advantage of Isabelle's automation, we illustrate our method with the formalisation in Isabelle/HOL of a mathematical notion developed in the 1980s: strict omegacategories. @InProceedings{CPP23p78, author = {Anthony Bordg and Adrián Doña Mateo}, title = {Encoding DependentlyTyped Constructions into Simple Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7889}, doi = {10.1145/3573105.3575679}, year = {2023}, } Publisher's Version 

Campbell, Eric Hayden 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Canu, Quentin 
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon , Quentin Canu , and PierreYves Strub (Inria, France; École Polytechnique, France; Meta, France) The purpose of this paper is the formal verification of a counterexample of Santos et al. to the socalled Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the penandpaper proof, our approach is entirely computational: we have implemented in Coq and proved correct an algorithm that explicitly computes, within the proof assistant, vertexedge graphs of polytopes as well as their diameter. The originality of this certificatebased algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over prooforiented data types and the correspondence with a lowlevel implementation over computationoriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g. matrix multiplications, basic routines on graphs), in order to make the derivation of the correctness of the lowlevel implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples to Hirsch conjecture due to Matschke, Santos and Weibel, respectively 20 and 23dimensional polytopes with 36425 and 73224 vertices involving rational coefficients with up to 20 digits. We also illustrate the performance of the method by computing the list of vertices or the diameter of wellknown classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem. @InProceedings{CPP23p17, author = {Xavier Allamigeon and Quentin Canu and PierreYves Strub}, title = {A Formal Disproof of Hirsch Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1729}, doi = {10.1145/3573105.3575678}, year = {2023}, } Publisher's Version 

Chen, John 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Clune, Joshua 
CPP '23: "A Formalized Reduction of ..."
A Formalized Reduction of Keller’s Conjecture
Joshua Clune (Carnegie Mellon University, USA) Keller’s conjecture in d dimensions states that there are no facesharefree tilings of ddimensional space by translates of a ddimensional cube. In 2020, Brakensiek et al. resolved this 90yearold conjecture by proving that the largest number of dimensions for which no facesharefree tilings exist is 7. This result, as well as many others pertaining to Keller’s conjecture, critically relies on a reduction from Keller’s original conjecture to a statement about cliques in generalized Keller graphs. In this paper, we present a formalization of this reduction in the Lean 3 theorem prover. Additionally, we combine this formalized reduction with the verification of a large clique in the Keller graph G_{8} to obtain the first verified endtoend proof that Keller’s conjecture is false in 8 dimensions. @InProceedings{CPP23p90, author = {Joshua Clune}, title = {A Formalized Reduction of Keller’s Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {90101}, doi = {10.1145/3573105.3575669}, year = {2023}, } Publisher's Version 

Cohen, Cyril 
CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using sFinite Kernels in Coq
Reynald Affeldt , Cyril Cohen , and Ayumu Saito (AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan) Probabilistic programming languages are used to write probabilistic models to make probabilistic inferences. A number of rigorous semantics have recently been proposed that are now available to carry out formal verification of probabilistic programs. In this paper, we extend an existing formalization of measure and integration theory with sfinite kernels, a mathematical structure to interpret typing judgments in the semantics of a probabilistic programming language. The resulting library makes it possible to reason formally about transformations of probabilistic programs and their execution. @InProceedings{CPP23p3, author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito}, title = {Semantics of Probabilistic Programs using sFinite Kernels in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {316}, doi = {10.1145/3573105.3575691}, year = {2023}, } Publisher's Version 

Coppola, Nirvana 
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen , Alex J. Best , Nirvana Coppola , and Sander R. Dahmen (Vrije Universiteit Amsterdam, Netherlands) Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y^{2}=x^{3}+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One nonelementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond. @InProceedings{CPP23p47, author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen}, title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4762}, doi = {10.1145/3573105.3575682}, year = {2023}, } Publisher's Version Info 

Cousineau, Denis 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Crance, Enzo 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Daggitt, Matthew L. 
CPP '23: "Compiling HigherOrder Specifications ..."
Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt , Robert Atkey , Wen Kokke , Ekaterina Komendantskaya , and Luca Arnaboldi (HeriotWatt University, UK; University of Strathclyde, UK; University of Edinburgh, UK) Modern verification tools frequently rely on compiling highlevel specifications to SMT queries. However, the highlevel specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unificationbased typechecker with type classes and automatic generalisation. Concretely, typechecking is used as a constructive procedure for underapproximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda. @InProceedings{CPP23p102, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102120}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version Info 

Dahmen, Sander R. 
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen , Alex J. Best , Nirvana Coppola , and Sander R. Dahmen (Vrije Universiteit Amsterdam, Netherlands) Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form y^{2}=x^{3}+d, where d is a (given) nonzero integer number and all solutions in integers x and y have to be determined. One nonelementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of d<0. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover, we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond. @InProceedings{CPP23p47, author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen}, title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4762}, doi = {10.1145/3573105.3575682}, year = {2023}, } Publisher's Version Info 

Degenne, Rémy 
CPP '23: "A Formalization of Doob’s ..."
A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying and Rémy Degenne (University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198CRIStAL, France) We present the formalization of Doob’s martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in L^{1}. In order to formalize those results, we build a definition of the conditional expectation in Banach spaces and develop the theory of stochastic processes, stopping times and martingales. As an application of the convergence theorems, we also present the formalization of Lévy’s generalized BorelCantelli lemma. This work on martingale theory is one of the first developments of probability theory in mathlib, and it builds upon diverse parts of that library such as topology, analysis and most importantly measure theory. @InProceedings{CPP23p334, author = {Kexing Ying and Rémy Degenne}, title = {A Formalization of Doob’s Martingale Convergence Theorems in mathlib}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {334347}, doi = {10.1145/3573105.3575675}, year = {2023}, } Publisher's Version 

DelignatLavaud, Antoine 
CPP '23: "ASN1*: Provably Correct, Nonmalleable ..."
ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER
Haobin Ni , Antoine DelignatLavaud , Cédric Fournet , Tahina Ramananandro , and Nikhil Swamy (Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA) Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITUT and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its nonmalleable binary format: for a given ASN.1 data type, every value has a distinct, unique binary representation. ASN.1 DER is used in many securitycritical interfaces for telecommunications and networking, such as the X.509 public key infrastructure, where nonmalleability is essential. However, due to the expressiveness and flexibility of the generalpurpose ASN.1 language, correctly parsing ASN.1 DER data formats is still considered a serious security challenge in practice. We present ASN1*, the first formalization of ASN.1 DER with a mechanized proof of nonmalleability. Our development provides a shallow embedding of ASN.1 in the F* proof assistant and formalizes its DER semantics within the EverParse parser generator framework. It guarantees that any ASN.1 data encoded using our DER semantics is nonmalleable. It yields verified code that parses valid binary representations into values of the corresponding ASN.1 data type while rejecting invalid ones. We empirically confirm that our semantics models ASN.1 DER usage in practice by evaluating ASN1* parsers extracted to OCaml on both positive and negative test cases involving X.509 certificates and Certificate Revocation Lists (CRLs). @InProceedings{CPP23p275, author = {Haobin Ni and Antoine DelignatLavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275289}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version 

Demange, Delphine 
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz , Delphine Demange , and Sandrine Blazy (Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France) The Gated Static Single Assignment (GSA) form was proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analyses and optimisation passes in compilers. Compared to SSA, GSA records additional data dependencies and provides more context, making optimisations more effective and allowing one to reason about programs as dataflow graphs. Many practical implementations have been proposed that follow, more or less faithfully, Ottenstein et al.'s seminal paper. But many discrepancies remain between these, depending on the kind of dependencies they are supposed to track and to leverage in analyses and code optimisations. In this paper, we present a formal semantics for GSA, mechanised in Coq. In particular, we clarify the nature and the purpose of gates in GSA, and define controlflow insensitive semantics for them. We provide a specification that can be used as a reference description for GSA. We also specify a translation from SSA to GSA and prove that this specification is semanticspreserving. We demonstrate that the approach is practical by implementing the specification as a validated translation within the CompCertSSA verified compiler. @InProceedings{CPP23p182, author = {Yann Herklotz and Delphine Demange and Sandrine Blazy}, title = {Mechanised Semantics for Gated Static Single Assignment}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {182196}, doi = {10.1145/3573105.3575681}, year = {2023}, } Publisher's Version 

De Prisque, Louise Dubois 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Doenges, Ryan 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Doña Mateo, Adrián 
CPP '23: "Encoding DependentlyTyped ..."
Encoding DependentlyTyped Constructions into Simple Type Theory
Anthony Bordg and Adrián Doña Mateo (University of Cambridge, UK; University of Edinburgh, UK) In this article, we show how one can formalise in type theory mathematical objects, for which dependent types are usually deemed unavoidable, using only simple types. We outline a method to encode most of the terms of Lean's dependent type theory into the simple type theory of Isabelle/HOL. Taking advantage of Isabelle's automation, we illustrate our method with the formalisation in Isabelle/HOL of a mathematical notion developed in the 1980s: strict omegacategories. @InProceedings{CPP23p78, author = {Anthony Bordg and Adrián Doña Mateo}, title = {Encoding DependentlyTyped Constructions into Simple Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7889}, doi = {10.1145/3573105.3575679}, year = {2023}, } Publisher's Version 

Edmonds, Chelsea 
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki KoutsoukouArgyraki , Mantas Bakšys , and Chelsea Edmonds (University of Cambridge, UK) We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers’s proof deriving the first effective bounds for Szemerédi’s Theorem. The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects. This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging. We demonstrate how locales, Isabelle’s module system, can be employed to handle such interplays in mathematical formalisations. To treat the graphtheoretic aspects of the proof, we make use of a new, more general undirected graph theory library developed by Edmonds, which is both flexible and extensible. In addition to the main theorem, which, following our source, is formulated for difference sets, we also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality. We moreover formalise a few additional results in additive combinatorics that are not used in the proof of the main theorem. This is the first formalisation of the Balog–Szemerédi–Gowers Theorem in any proof assistant to our knowledge. @InProceedings{CPP23p225, author = {Angeliki KoutsoukouArgyraki and Mantas Bakšys and Chelsea Edmonds}, title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {225238}, doi = {10.1145/3573105.3575680}, year = {2023}, } Publisher's Version 

Färber, Michael 
CPP '23: "Terms for Efficient Proof ..."
Terms for Efficient Proof Checking and Parsing
Michael Färber (University of Innsbruck, Austria) Proofs automatically generated by interactive or automated theorem provers are often several orders of magnitude larger than proofs written by hand. This implies significant challenges for processing such proofs efficiently. It turns out that the data structures used to encode terms have a high impact on performance. This article proposes several term data structures; in particular, heterogeneous terms for proof checking that distinguish long and shortlived terms, and abstract terms for proof parsing. Both term data structures are implemented in the proof checker Kontroli, enabling it to parse and check proofs both sequentially and concurrently without overhead. The evaluation on three datasets exported from interactive theorem provers shows that the new term data structures significantly improve proof checking performance. @InProceedings{CPP23p135, author = {Michael Färber}, title = {Terms for Efficient Proof Checking and Parsing}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {135147}, doi = {10.1145/3573105.3575686}, year = {2023}, } Publisher's Version 

Férée, Hugo 
CPP '23: "Formalizing and Computing ..."
Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool (Université Paris Cité, France) A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of ∃ p φ and ∀ p φ from p and φ. @InProceedings{CPP23p148, author = {Hugo Férée and Sam van Gool}, title = {Formalizing and Computing Propositional Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {148158}, doi = {10.1145/3573105.3575668}, year = {2023}, } Publisher's Version Info 

Forster, Yannick 
CPP '23: "A Computational CantorBernstein ..."
A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster , Felix Jahn , and Gert Smolka (Inria, France; Saarland University, Germany) The CantorBernstein theorem (CB) from set theory, stating that two sets which can be injectively embedded into each other are in bijection, is inherently classical in its full generality, i.e. implies the law of excluded middle, a result due to Pradic and Brown. Recently, Escardó has provided a proof of CB in univalent type theory, assuming the law of excluded middle. It is a natural question to ask which restrictions of CB can be proved without axiomatic assumptions. We give a partial answer to this question contributing an assumptionfree proof of CB restricted to enumerable discrete types, i.e. types which can be computationally treated. In fact, we construct several bijections from injections: The first is by translating a proof of the Myhill isomorphism theorem from computability theory – stating that 1equivalent predicates are recursively isomorphic – to constructive type theory, where the bijection is constructed in stages and an algorithm with an intricate termination argument is used to extend the bijection in every step. The second is also constructed in stages, but with a simpler extension algorithm sufficient for CB. The third is constructed directly in such a way that it only relies on the given enumerations of the types, not on the given injections. We aim at keeping the explanations simple, accessible, and concise in the style of a “proof pearl”. All proofs are machinechecked in Coq but should transport to other foundations – they do not rely on impredicativity, on choice principles, or on large eliminations. @InProceedings{CPP23p159, author = {Yannick Forster and Felix Jahn and Gert Smolka}, title = {A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {159166}, doi = {10.1145/3573105.3575690}, year = {2023}, } Publisher's Version 

Foster, Nate 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Fournet, Cédric 
CPP '23: "ASN1*: Provably Correct, Nonmalleable ..."
ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER
Haobin Ni , Antoine DelignatLavaud , Cédric Fournet , Tahina Ramananandro , and Nikhil Swamy (Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA) Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITUT and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its nonmalleable binary format: for a given ASN.1 data type, every value has a distinct, unique binary representation. ASN.1 DER is used in many securitycritical interfaces for telecommunications and networking, such as the X.509 public key infrastructure, where nonmalleability is essential. However, due to the expressiveness and flexibility of the generalpurpose ASN.1 language, correctly parsing ASN.1 DER data formats is still considered a serious security challenge in practice. We present ASN1*, the first formalization of ASN.1 DER with a mechanized proof of nonmalleability. Our development provides a shallow embedding of ASN.1 in the F* proof assistant and formalizes its DER semantics within the EverParse parser generator framework. It guarantees that any ASN.1 data encoded using our DER semantics is nonmalleable. It yields verified code that parses valid binary representations into values of the corresponding ASN.1 data type while rejecting invalid ones. We empirically confirm that our semantics models ASN.1 DER usage in practice by evaluating ASN1* parsers extracted to OCaml on both positive and negative test cases involving X.509 certificates and Certificate Revocation Lists (CRLs). @InProceedings{CPP23p275, author = {Haobin Ni and Antoine DelignatLavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275289}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version 

From, Asta Halkjær 
CPP '23: "Aesop: WhiteBox BestFirst ..."
Aesop: WhiteBox BestFirst Proof Search for Lean
Jannis Limperg and Asta Halkjær From (Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark) We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a treebased search over a userspecified set of proof rules. It supports safe and unsafe rules and uses a bestfirst search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a whitebox proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a bestfirst search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for bestfirst search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows. @InProceedings{CPP23p253, author = {Jannis Limperg and Asta Halkjær From}, title = {Aesop: WhiteBox BestFirst Proof Search for Lean}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253266}, doi = {10.1145/3573105.3575671}, year = {2023}, } Publisher's Version 

Fromherz, Aymeric 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Grégoire, Benjamin 
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi
Benjamin Grégoire , JeanChristophe Léchenet , and Enrico Tassi (Université Côte d’Azur, France; Inria, France) In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention. @InProceedings{CPP23p167, author = {Benjamin Grégoire and JeanChristophe Léchenet and Enrico Tassi}, title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {167181}, doi = {10.1145/3573105.3575683}, year = {2023}, } Publisher's Version 

Hayes, Ian J. 
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb , Ian J. Hayes , and Mark Utting (University of Queensland, Australia) Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules. @InProceedings{CPP23p320, author = {Brae J. Webb and Ian J. Hayes and Mark Utting}, title = {Verifying Term Graph Optimizations using Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {320333}, doi = {10.1145/3573105.3575673}, year = {2023}, } Publisher's Version 

Herklotz, Yann 
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz , Delphine Demange , and Sandrine Blazy (Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France) The Gated Static Single Assignment (GSA) form was proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analyses and optimisation passes in compilers. Compared to SSA, GSA records additional data dependencies and provides more context, making optimisations more effective and allowing one to reason about programs as dataflow graphs. Many practical implementations have been proposed that follow, more or less faithfully, Ottenstein et al.'s seminal paper. But many discrepancies remain between these, depending on the kind of dependencies they are supposed to track and to leverage in analyses and code optimisations. In this paper, we present a formal semantics for GSA, mechanised in Coq. In particular, we clarify the nature and the purpose of gates in GSA, and define controlflow insensitive semantics for them. We provide a specification that can be used as a reference description for GSA. We also specify a translation from SSA to GSA and prove that this specification is semanticspreserving. We demonstrate that the approach is practical by implementing the specification as a validated translation within the CompCertSSA verified compiler. @InProceedings{CPP23p182, author = {Yann Herklotz and Delphine Demange and Sandrine Blazy}, title = {Mechanised Semantics for Gated Static Single Assignment}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {182196}, doi = {10.1145/3573105.3575681}, year = {2023}, } Publisher's Version 

Hietala, Kesha 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Isak, Natalie 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Jahn, Felix 
CPP '23: "A Computational CantorBernstein ..."
A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster , Felix Jahn , and Gert Smolka (Inria, France; Saarland University, Germany) The CantorBernstein theorem (CB) from set theory, stating that two sets which can be injectively embedded into each other are in bijection, is inherently classical in its full generality, i.e. implies the law of excluded middle, a result due to Pradic and Brown. Recently, Escardó has provided a proof of CB in univalent type theory, assuming the law of excluded middle. It is a natural question to ask which restrictions of CB can be proved without axiomatic assumptions. We give a partial answer to this question contributing an assumptionfree proof of CB restricted to enumerable discrete types, i.e. types which can be computationally treated. In fact, we construct several bijections from injections: The first is by translating a proof of the Myhill isomorphism theorem from computability theory – stating that 1equivalent predicates are recursively isomorphic – to constructive type theory, where the bijection is constructed in stages and an algorithm with an intricate termination argument is used to extend the bijection in every step. The second is also constructed in stages, but with a simpler extension algorithm sufficient for CB. The third is constructed directly in such a way that it only relies on the given enumerations of the types, not on the given injections. We aim at keeping the explanations simple, accessible, and concise in the style of a “proof pearl”. All proofs are machinechecked in Coq but should transport to other foundations – they do not rely on impredicativity, on choice principles, or on large eliminations. @InProceedings{CPP23p159, author = {Yannick Forster and Felix Jahn and Gert Smolka}, title = {A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {159166}, doi = {10.1145/3573105.3575690}, year = {2023}, } Publisher's Version 

Kaliszyk, Cezary 
CPP '23: "Improved Assistance for Interactive ..."
Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk (University of Innsbruck, Austria) Machine learning techniques have been included in various theorem proving tools for approximately two decades. Some of the learning tasks are well understood and tools actually help practitioners, while other tasks are still in their early developmental stages. In this talk I will try to classify the various learning tasks and discuss the learning techniques and tools that are aimed at enhancing the efficiency of interactive theorem provers. I will discuss the most successful techniques aimed at improving the power of automation, that use MonteCarlo simulations guided by reinforcement learning from previous proof attempts. I will also consider the present and the future challenges including more efficient interaction with interactive theorem provers. @InProceedings{CPP23p2, author = {Cezary Kaliszyk}, title = {Improved Assistance for Interactive Proof (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {22}, doi = {10.1145/3573105.3579108}, year = {2023}, } Publisher's Version 

Keller, Chantal 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Kohl, Christina 
CPP '23: "A Formalization of the Development ..."
A Formalization of the Development Closedness Criterion for LeftLinear Term Rewrite Systems
Christina Kohl and Aart Middeldorp (University of Innsbruck, Austria) Several critical pair criteria are known that guarantee confluence of leftlinear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requires a high level of understanding about overlapping redexes and descendants as well as several intermediate results related to these concepts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA. @InProceedings{CPP23p197, author = {Christina Kohl and Aart Middeldorp}, title = {A Formalization of the Development Closedness Criterion for LeftLinear Term Rewrite Systems}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {197210}, doi = {10.1145/3573105.3575667}, year = {2023}, } Publisher's Version Info 

Kokke, Wen 
CPP '23: "Compiling HigherOrder Specifications ..."
Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt , Robert Atkey , Wen Kokke , Ekaterina Komendantskaya , and Luca Arnaboldi (HeriotWatt University, UK; University of Strathclyde, UK; University of Edinburgh, UK) Modern verification tools frequently rely on compiling highlevel specifications to SMT queries. However, the highlevel specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unificationbased typechecker with type classes and automatic generalisation. Concretely, typechecking is used as a constructive procedure for underapproximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda. @InProceedings{CPP23p102, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102120}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version Info 

Komendantskaya, Ekaterina 
CPP '23: "Compiling HigherOrder Specifications ..."
Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt , Robert Atkey , Wen Kokke , Ekaterina Komendantskaya , and Luca Arnaboldi (HeriotWatt University, UK; University of Strathclyde, UK; University of Edinburgh, UK) Modern verification tools frequently rely on compiling highlevel specifications to SMT queries. However, the highlevel specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unificationbased typechecker with type classes and automatic generalisation. Concretely, typechecking is used as a constructive procedure for underapproximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda. @InProceedings{CPP23p102, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling HigherOrder Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102120}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version Info 

Kosaian, Katherine 
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian , Yong Kiam Tan , and André Platzer (Carnegie Mellon University, USA; KIT, Germany) We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the firstorder logic of real arithmetic to a logically equivalent quantifierfree formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the BenOr, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL. @InProceedings{CPP23p211, author = {Katherine Kosaian and Yong Kiam Tan and André Platzer}, title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {211224}, doi = {10.1145/3573105.3575672}, year = {2023}, } Publisher's Version 

KoutsoukouArgyraki, Angeliki 
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki KoutsoukouArgyraki , Mantas Bakšys , and Chelsea Edmonds (University of Cambridge, UK) We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers’s proof deriving the first effective bounds for Szemerédi’s Theorem. The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects. This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging. We demonstrate how locales, Isabelle’s module system, can be employed to handle such interplays in mathematical formalisations. To treat the graphtheoretic aspects of the proof, we make use of a new, more general undirected graph theory library developed by Edmonds, which is both flexible and extensible. In addition to the main theorem, which, following our source, is formulated for difference sets, we also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality. We moreover formalise a few additional results in additive combinatorics that are not used in the proof of the main theorem. This is the first formalisation of the Balog–Szemerédi–Gowers Theorem in any proof assistant to our knowledge. @InProceedings{CPP23p225, author = {Angeliki KoutsoukouArgyraki and Mantas Bakšys and Chelsea Edmonds}, title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {225238}, doi = {10.1145/3573105.3575680}, year = {2023}, } Publisher's Version 

Lamiaux, Thomas 
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux , Axel Ljungström , and Anders Mörtberg (University of ParisSaclay, France; ENS ParisSaclay, France; Stockholm University, Sweden) In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence. @InProceedings{CPP23p239, author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg}, title = {Computing Cohomology Rings in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {239252}, doi = {10.1145/3573105.3575677}, year = {2023}, } Publisher's Version 

Léchenet, JeanChristophe 
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi
Benjamin Grégoire , JeanChristophe Léchenet , and Enrico Tassi (Université Côte d’Azur, France; Inria, France) In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention. @InProceedings{CPP23p167, author = {Benjamin Grégoire and JeanChristophe Léchenet and Enrico Tassi}, title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {167181}, doi = {10.1145/3573105.3575683}, year = {2023}, } Publisher's Version 

Limperg, Jannis 
CPP '23: "Aesop: WhiteBox BestFirst ..."
Aesop: WhiteBox BestFirst Proof Search for Lean
Jannis Limperg and Asta Halkjær From (Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark) We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a treebased search over a userspecified set of proof rules. It supports safe and unsafe rules and uses a bestfirst search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a whitebox proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a bestfirst search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for bestfirst search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows. @InProceedings{CPP23p253, author = {Jannis Limperg and Asta Halkjær From}, title = {Aesop: WhiteBox BestFirst Proof Search for Lean}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253266}, doi = {10.1145/3573105.3575671}, year = {2023}, } Publisher's Version 

Ljungström, Axel 
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux , Axel Ljungström , and Anders Mörtberg (University of ParisSaclay, France; ENS ParisSaclay, France; Stockholm University, Sweden) In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence. @InProceedings{CPP23p239, author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg}, title = {Computing Cohomology Rings in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {239252}, doi = {10.1145/3573105.3575677}, year = {2023}, } Publisher's Version 

Mahboubi, Assia 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Massot, Patrick 
CPP '23: "Formalising the hPrinciple ..."
Formalising the hPrinciple and Sphere Eversion
Floris van Doorn , Patrick Massot , and Oliver Nash (University of ParisSaclay, France; CNRS, France; Imperial College London, UK) In differential topology and geometry, the hprinciple is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local hprinciple for firstorder open and ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in geometry. In particular it reproves Smale’s celebrated sphere eversion theorem, a visually striking and counterintuitive construction. Our formalisation uses Theillière’s implementation of convex integration from 2018. This paper reports on the first part of the sphere eversion project formalising the global version of the hprinciple for open and ample first order differential relations, for maps between smooth manifolds. The local version for vector spaces described in this paper is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraicallyflavoured mathematics. @InProceedings{CPP23p121, author = {Floris van Doorn and Patrick Massot and Oliver Nash}, title = {Formalising the hPrinciple and Sphere Eversion}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {121134}, doi = {10.1145/3573105.3575688}, year = {2023}, } Publisher's Version Published Artifact Info Artifacts Available 

Mehta, Bhavik 
CPP '23: "Formalising Sharkovsky’s ..."
Formalising Sharkovsky’s Theorem (Proof Pearl)
Bhavik Mehta (University of Cambridge, UK) Sharkovsky's theorem is a celebrated result by Ukrainian mathematician Oleksandr Sharkovsky in the theory of discrete dynamical systems, including the fact that if a continuous function of reals has a point of period 3, it must have points of any period. We formalise the proof in the Lean theorem prover, giving a characterisation of the possible sets of periods a continuous function on the real numbers may have. We further include the converse of the theorem, showing that the aforementioned sets are achievable under mild conditions. @InProceedings{CPP23p267, author = {Bhavik Mehta}, title = {Formalising Sharkovsky’s Theorem (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {267274}, doi = {10.1145/3573105.3575689}, year = {2023}, } Publisher's Version Info 

Middeldorp, Aart 
CPP '23: "A Formalization of the Development ..."
A Formalization of the Development Closedness Criterion for LeftLinear Term Rewrite Systems
Christina Kohl and Aart Middeldorp (University of Innsbruck, Austria) Several critical pair criteria are known that guarantee confluence of leftlinear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requires a high level of understanding about overlapping redexes and descendants as well as several intermediate results related to these concepts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA. @InProceedings{CPP23p197, author = {Christina Kohl and Aart Middeldorp}, title = {A Formalization of the Development Closedness Criterion for LeftLinear Term Rewrite Systems}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {197210}, doi = {10.1145/3573105.3575667}, year = {2023}, } Publisher's Version Info 

Mörtberg, Anders 
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux , Axel Ljungström , and Anders Mörtberg (University of ParisSaclay, France; ENS ParisSaclay, France; Stockholm University, Sweden) In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence. @InProceedings{CPP23p239, author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg}, title = {Computing Cohomology Rings in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {239252}, doi = {10.1145/3573105.3575677}, year = {2023}, } Publisher's Version 

Nash, Oliver 
CPP '23: "Formalising the hPrinciple ..."
Formalising the hPrinciple and Sphere Eversion
Floris van Doorn , Patrick Massot , and Oliver Nash (University of ParisSaclay, France; CNRS, France; Imperial College London, UK) In differential topology and geometry, the hprinciple is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local hprinciple for firstorder open and ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in geometry. In particular it reproves Smale’s celebrated sphere eversion theorem, a visually striking and counterintuitive construction. Our formalisation uses Theillière’s implementation of convex integration from 2018. This paper reports on the first part of the sphere eversion project formalising the global version of the hprinciple for open and ample first order differential relations, for maps between smooth manifolds. The local version for vector spaces described in this paper is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraicallyflavoured mathematics. @InProceedings{CPP23p121, author = {Floris van Doorn and Patrick Massot and Oliver Nash}, title = {Formalising the hPrinciple and Sphere Eversion}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {121134}, doi = {10.1145/3573105.3575688}, year = {2023}, } Publisher's Version Published Artifact Info Artifacts Available 

Ni, Haobin 
CPP '23: "ASN1*: Provably Correct, Nonmalleable ..."
ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER
Haobin Ni , Antoine DelignatLavaud , Cédric Fournet , Tahina Ramananandro , and Nikhil Swamy (Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA) Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITUT and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its nonmalleable binary format: for a given ASN.1 data type, every value has a distinct, unique binary representation. ASN.1 DER is used in many securitycritical interfaces for telecommunications and networking, such as the X.509 public key infrastructure, where nonmalleability is essential. However, due to the expressiveness and flexibility of the generalpurpose ASN.1 language, correctly parsing ASN.1 DER data formats is still considered a serious security challenge in practice. We present ASN1*, the first formalization of ASN.1 DER with a mechanized proof of nonmalleability. Our development provides a shallow embedding of ASN.1 in the F* proof assistant and formalizes its DER semantics within the EverParse parser generator framework. It guarantees that any ASN.1 data encoded using our DER semantics is nonmalleable. It yields verified code that parses valid binary representations into values of the corresponding ASN.1 data type while rejecting invalid ones. We empirically confirm that our semantics models ASN.1 DER usage in practice by evaluating ASN1* parsers extracted to OCaml on both positive and negative test cases involving X.509 certificates and Certificate Revocation Lists (CRLs). @InProceedings{CPP23p275, author = {Haobin Ni and Antoine DelignatLavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275289}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version 

Nielsen, Eske Hoy 
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen , Danil Annenkov , and Bas Spitters (Aarhus University, Denmark) The number of attacks and accidents leading to significant losses of cryptoassets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, noncustodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter’s implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns. @InProceedings{CPP23p290, author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters}, title = {Formalising Decentralised Exchanges in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {290302}, doi = {10.1145/3573105.3575685}, year = {2023}, } Publisher's Version 

Parno, Bryan 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Peterson, Rudy 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Platzer, André 
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian , Yong Kiam Tan , and André Platzer (Carnegie Mellon University, USA; KIT, Germany) We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the firstorder logic of real arithmetic to a logically equivalent quantifierfree formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the BenOr, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL. @InProceedings{CPP23p211, author = {Katherine Kosaian and Yong Kiam Tan and André Platzer}, title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {211224}, doi = {10.1145/3573105.3575672}, year = {2023}, } Publisher's Version 

Ramamurthy, Ravi 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Ramananandro, Tahina 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info CPP '23: "ASN1*: Provably Correct, Nonmalleable ..." ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER Haobin Ni , Antoine DelignatLavaud , Cédric Fournet , Tahina Ramananandro , and Nikhil Swamy (Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA) Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITUT and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its nonmalleable binary format: for a given ASN.1 data type, every value has a distinct, unique binary representation. ASN.1 DER is used in many securitycritical interfaces for telecommunications and networking, such as the X.509 public key infrastructure, where nonmalleability is essential. However, due to the expressiveness and flexibility of the generalpurpose ASN.1 language, correctly parsing ASN.1 DER data formats is still considered a serious security challenge in practice. We present ASN1*, the first formalization of ASN.1 DER with a mechanized proof of nonmalleability. Our development provides a shallow embedding of ASN.1 in the F* proof assistant and formalizes its DER semantics within the EverParse parser generator framework. It guarantees that any ASN.1 data encoded using our DER semantics is nonmalleable. It yields verified code that parses valid binary representations into values of the corresponding ASN.1 data type while rejecting invalid ones. We empirically confirm that our semantics models ASN.1 DER usage in practice by evaluating ASN1* parsers extracted to OCaml on both positive and negative test cases involving X.509 certificates and Certificate Revocation Lists (CRLs). @InProceedings{CPP23p275, author = {Haobin Ni and Antoine DelignatLavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275289}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version 

Rastogi, Aseem 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info 

Saito, Ayumu 
CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using sFinite Kernels in Coq
Reynald Affeldt , Cyril Cohen , and Ayumu Saito (AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan) Probabilistic programming languages are used to write probabilistic models to make probabilistic inferences. A number of rigorous semantics have recently been proposed that are now available to carry out formal verification of probabilistic programs. In this paper, we extend an existing formalization of measure and integration theory with sfinite kernels, a mathematical structure to interpret typing judgments in the semantics of a probabilistic programming language. The resulting library makes it possible to reason formally about transformations of probabilistic programs and their execution. @InProceedings{CPP23p3, author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito}, title = {Semantics of Probabilistic Programs using sFinite Kernels in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {316}, doi = {10.1145/3573105.3575691}, year = {2023}, } Publisher's Version 

Shyu, Calvin 
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson , Eric Hayden Campbell , John Chen , Natalie Isak , Calvin Shyu , Ryan Doenges , Parisa Ataei , and Nate Foster (Cornell University, USA; Microsoft, USA) P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domainspecific features of P4 itself. P4Cub has a frontend based on Petr4, and has been fully mechanized in Coq including bigstep and smallstep semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. @InProceedings{CPP23p303, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {303319}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Smolka, Gert 
CPP '23: "A Computational CantorBernstein ..."
A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster , Felix Jahn , and Gert Smolka (Inria, France; Saarland University, Germany) The CantorBernstein theorem (CB) from set theory, stating that two sets which can be injectively embedded into each other are in bijection, is inherently classical in its full generality, i.e. implies the law of excluded middle, a result due to Pradic and Brown. Recently, Escardó has provided a proof of CB in univalent type theory, assuming the law of excluded middle. It is a natural question to ask which restrictions of CB can be proved without axiomatic assumptions. We give a partial answer to this question contributing an assumptionfree proof of CB restricted to enumerable discrete types, i.e. types which can be computationally treated. In fact, we construct several bijections from injections: The first is by translating a proof of the Myhill isomorphism theorem from computability theory – stating that 1equivalent predicates are recursively isomorphic – to constructive type theory, where the bijection is constructed in stages and an algorithm with an intricate termination argument is used to extend the bijection in every step. The second is also constructed in stages, but with a simpler extension algorithm sufficient for CB. The third is constructed directly in such a way that it only relies on the given enumerations of the types, not on the given injections. We aim at keeping the explanations simple, accessible, and concise in the style of a “proof pearl”. All proofs are machinechecked in Coq but should transport to other foundations – they do not rely on impredicativity, on choice principles, or on large eliminations. @InProceedings{CPP23p159, author = {Yannick Forster and Felix Jahn and Gert Smolka}, title = {A Computational CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {159166}, doi = {10.1145/3573105.3575690}, year = {2023}, } Publisher's Version 

Spitters, Bas 
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen , Danil Annenkov , and Bas Spitters (Aarhus University, Denmark) The number of attacks and accidents leading to significant losses of cryptoassets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, noncustodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter’s implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns. @InProceedings{CPP23p290, author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters}, title = {Formalising Decentralised Exchanges in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {290302}, doi = {10.1145/3573105.3575685}, year = {2023}, } Publisher's Version 

Strub, PierreYves 
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon , Quentin Canu , and PierreYves Strub (Inria, France; École Polytechnique, France; Meta, France) The purpose of this paper is the formal verification of a counterexample of Santos et al. to the socalled Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the penandpaper proof, our approach is entirely computational: we have implemented in Coq and proved correct an algorithm that explicitly computes, within the proof assistant, vertexedge graphs of polytopes as well as their diameter. The originality of this certificatebased algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over prooforiented data types and the correspondence with a lowlevel implementation over computationoriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g. matrix multiplications, basic routines on graphs), in order to make the derivation of the correctness of the lowlevel implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples to Hirsch conjecture due to Matschke, Santos and Weibel, respectively 20 and 23dimensional polytopes with 36425 and 73224 vertices involving rational coefficients with up to 20 digits. We also illustrate the performance of the method by computing the list of vertices or the diameter of wellknown classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem. @InProceedings{CPP23p17, author = {Xavier Allamigeon and Quentin Canu and PierreYves Strub}, title = {A Formal Disproof of Hirsch Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1729}, doi = {10.1145/3573105.3575678}, year = {2023}, } Publisher's Version 

Swamy, Nikhil 
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores
Arvind Arasu , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Aymeric Fromherz , Kesha Hietala , Bryan Parno , and Ravi Ramamurthy (Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA) FastVer is a protocol that uses a variety of memorychecking techniques to monitor the integrity of keyvalue stores with only a modest runtime cost. Arasu et al. formalize the highlevel design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementationFastVer is implemented in unverified C++ code. In this work, we present FastVer2, a lowlevel, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's highlevel specification. Our proof is the first endtoend system proven using Steel, and in doing so we contribute new ghoststate constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future. @InProceedings{CPP23p30, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, KeyValue Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3046}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version Info CPP '23: "ASN1*: Provably Correct, Nonmalleable ..." ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER Haobin Ni , Antoine DelignatLavaud , Cédric Fournet , Tahina Ramananandro , and Nikhil Swamy (Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA) Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITUT and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its nonmalleable binary format: for a given ASN.1 data type, every value has a distinct, unique binary representation. ASN.1 DER is used in many securitycritical interfaces for telecommunications and networking, such as the X.509 public key infrastructure, where nonmalleability is essential. However, due to the expressiveness and flexibility of the generalpurpose ASN.1 language, correctly parsing ASN.1 DER data formats is still considered a serious security challenge in practice. We present ASN1*, the first formalization of ASN.1 DER with a mechanized proof of nonmalleability. Our development provides a shallow embedding of ASN.1 in the F* proof assistant and formalizes its DER semantics within the EverParse parser generator framework. It guarantees that any ASN.1 data encoded using our DER semantics is nonmalleable. It yields verified code that parses valid binary representations into values of the corresponding ASN.1 data type while rejecting invalid ones. We empirically confirm that our semantics models ASN.1 DER usage in practice by evaluating ASN1* parsers extracted to OCaml on both positive and negative test cases involving X.509 certificates and Certificate Revocation Lists (CRLs). @InProceedings{CPP23p275, author = {Haobin Ni and Antoine DelignatLavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Nonmalleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275289}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version 

Tan, Yong Kiam 
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian , Yong Kiam Tan , and André Platzer (Carnegie Mellon University, USA; KIT, Germany) We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the firstorder logic of real arithmetic to a logically equivalent quantifierfree formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the BenOr, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL. @InProceedings{CPP23p211, author = {Katherine Kosaian and Yong Kiam Tan and André Platzer}, title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {211224}, doi = {10.1145/3573105.3575672}, year = {2023}, } Publisher's Version 

Tassi, Enrico 
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi
Benjamin Grégoire , JeanChristophe Léchenet , and Enrico Tassi (Université Côte d’Azur, France; Inria, France) In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention. @InProceedings{CPP23p167, author = {Benjamin Grégoire and JeanChristophe Léchenet and Enrico Tassi}, title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with CoqElpi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {167181}, doi = {10.1145/3573105.3575683}, year = {2023}, } Publisher's Version 

Utting, Mark 
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb , Ian J. Hayes , and Mark Utting (University of Queensland, Australia) Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules. @InProceedings{CPP23p320, author = {Brae J. Webb and Ian J. Hayes and Mark Utting}, title = {Verifying Term Graph Optimizations using Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {320333}, doi = {10.1145/3573105.3575673}, year = {2023}, } Publisher's Version 

Van Doorn, Floris 
CPP '23: "Formalising the hPrinciple ..."
Formalising the hPrinciple and Sphere Eversion
Floris van Doorn , Patrick Massot , and Oliver Nash (University of ParisSaclay, France; CNRS, France; Imperial College London, UK) In differential topology and geometry, the hprinciple is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local hprinciple for firstorder open and ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in geometry. In particular it reproves Smale’s celebrated sphere eversion theorem, a visually striking and counterintuitive construction. Our formalisation uses Theillière’s implementation of convex integration from 2018. This paper reports on the first part of the sphere eversion project formalising the global version of the hprinciple for open and ample first order differential relations, for maps between smooth manifolds. The local version for vector spaces described in this paper is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraicallyflavoured mathematics. @InProceedings{CPP23p121, author = {Floris van Doorn and Patrick Massot and Oliver Nash}, title = {Formalising the hPrinciple and Sphere Eversion}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {121134}, doi = {10.1145/3573105.3575688}, year = {2023}, } Publisher's Version Published Artifact Info Artifacts Available 

Van Gool, Sam 
CPP '23: "Formalizing and Computing ..."
Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool (Université Paris Cité, France) A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of ∃ p φ and ∀ p φ from p and φ. @InProceedings{CPP23p148, author = {Hugo Férée and Sam van Gool}, title = {Formalizing and Computing Propositional Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {148158}, doi = {10.1145/3573105.3575668}, year = {2023}, } Publisher's Version Info 

Vial, Pierre 
CPP '23: "Compositional Preprocessing ..."
Compositional Preprocessing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , Assia Mahboubi , and Pierre Vial (LMF, France; Inria, France; University of ParisSaclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France) In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of preprocessing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines. @InProceedings{CPP23p63, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Preprocessing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6377}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version 

Webb, Brae J. 
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb , Ian J. Hayes , and Mark Utting (University of Queensland, Australia) Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules. @InProceedings{CPP23p320, author = {Brae J. Webb and Ian J. Hayes and Mark Utting}, title = {Verifying Term Graph Optimizations using Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {320333}, doi = {10.1145/3573105.3575673}, year = {2023}, } Publisher's Version 

Ying, Kexing 
CPP '23: "A Formalization of Doob’s ..."
A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying and Rémy Degenne (University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198CRIStAL, France) We present the formalization of Doob’s martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in L^{1}. In order to formalize those results, we build a definition of the conditional expectation in Banach spaces and develop the theory of stochastic processes, stopping times and martingales. As an application of the convergence theorems, we also present the formalization of Lévy’s generalized BorelCantelli lemma. This work on martingale theory is one of the first developments of probability theory in mathlib, and it builds upon diverse parts of that library such as topology, analysis and most importantly measure theory. @InProceedings{CPP23p334, author = {Kexing Ying and Rémy Degenne}, title = {A Formalization of Doob’s Martingale Convergence Theorems in mathlib}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {334347}, doi = {10.1145/3573105.3575675}, year = {2023}, } Publisher's Version 
82 authors
proc time: 20.18