Workshop CPP 2018 – Author Index 
Contents 
Abstracts 
Authors

A B C D F G H J K L M N P R S T W Y Z
Amani, Sidney 
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples (Data61 at CSIRO, Australia; ENS ParisSaclay, France; University of ParisSaclay, France; UNSW, Australia) Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety, security, or missioncritical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straightline code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts. @InProceedings{CPP18p66, author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples}, title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6677}, doi = {10.1145/3167084}, year = {2018}, } Publisher's Version 

Bard, Joachim 
CPP '18: "Completeness and Decidability ..."
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal and Joachim Bard (University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Saarland University, Germany) The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are nonconstructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof by Kozen and Parikh into our constructive setting. We base our proof on a Prattstyle decision method for satisfiability constructing finite models for satisfiable formulas and pruning refutations for unsatisfiable formulas. Completeness of Segerberg's axiomatization of PDL is then obtained by translating pruning refutations to derivations in the Hilbert system. We first treat PDL without converse and then extend the proofs to Converse PDL. All results are formalized in Coq/Ssreflect. @InProceedings{CPP18p42, author = {Christian Doczkal and Joachim Bard}, title = {Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4252}, doi = {10.1145/3167088}, year = {2018}, } Publisher's Version 

Bégel, Myriam 
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples (Data61 at CSIRO, Australia; ENS ParisSaclay, France; University of ParisSaclay, France; UNSW, Australia) Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety, security, or missioncritical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straightline code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts. @InProceedings{CPP18p66, author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples}, title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6677}, doi = {10.1145/3167084}, year = {2018}, } Publisher's Version 

Biernacki, Dariusz 
CPP '18: "A Coq Formalization of Normalization ..."
A Coq Formalization of Normalization by Evaluation for MartinLöf Type Theory
Paweł Wieczorek and Dariusz Biernacki (University of Wrocław, Poland) We present a Coq formalization of the normalizationbyevaluation algorithm for MartinLöf dependent type theory with one universe and judgmental equality. The end results of the formalization are certified implementations of a reductionfree normalizer and of a decision procedure for term equality. The formalization takes advantage of a graphbased variant of the BoveCapretta method to encode mutually recursive evaluation functions with nested recursive calls. The proof of completeness, which uses the PERmodel of dependent types, is formalized by relying on impredicativity of the Coq system rather than on the commonly used inductionrecursion scheme which is not available in Coq. The proof of soundness is formalized by encoding logical relations as partial functions. @InProceedings{CPP18p266, author = {Paweł Wieczorek and Dariusz Biernacki}, title = {A Coq Formalization of Normalization by Evaluation for MartinLöf Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {266279}, doi = {10.1145/3167091}, year = {2018}, } Publisher's Version Info 

Blanchette, Jasmin Christian 
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich (Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA) Based on our earlier formalization of conflictdriven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further. @InProceedings{CPP18p158, author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich}, title = {A Verified SAT Solver with Watched Literals Using Imperative HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {158171}, doi = {10.1145/3167080}, year = {2018}, } Publisher's Version 

Bonacina, Maria Paola 
CPP '18: "Proofs in ConflictDriven ..."
Proofs in ConflictDriven Theory Combination
Maria Paola Bonacina, Stéphane GrahamLengrand, and Natarajan Shankar (University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA) Searchbased satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflictdriven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (ConflictDriven SATisfiability) is a method for conflictdriven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflictdriven SMTsolving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction. @InProceedings{CPP18p186, author = {Maria Paola Bonacina and Stéphane GrahamLengrand and Natarajan Shankar}, title = {Proofs in ConflictDriven Theory Combination}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {186200}, doi = {10.1145/3167096}, year = {2018}, } Publisher's Version 

Bortin, Maksym 
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples (Data61 at CSIRO, Australia; ENS ParisSaclay, France; University of ParisSaclay, France; UNSW, Australia) Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety, security, or missioncritical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straightline code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts. @InProceedings{CPP18p66, author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples}, title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6677}, doi = {10.1145/3167084}, year = {2018}, } Publisher's Version 

Breitner, Joachim 
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal SpectorZabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich (University of Pennsylvania, USA) We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hstocoq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies – a lawful Monad instance, “Hutton’s razor”, and an existing data structure library – and prove their correctness. These examples show that this approach is viable: both that hstocoq applies to existing Haskell code, and that the output it produces is amenable to verification. @InProceedings{CPP18p14, author = {Antal SpectorZabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich}, title = {Total Haskell is Reasonable Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1427}, doi = {10.1145/3167092}, year = {2018}, } Publisher's Version Info 

Chaudhuri, Kaustuv 
CPP '18: "A TwoLevel Logic Perspective ..."
A TwoLevel Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri (Inria, France; École Polytechnique, France) Lambdatree syntax (λTS), also known as higherorder abstract syntax (HOAS), is a representational technique where the pure λcalculus in a metalanguage is used to represent binding constructs in an object language. A key feature of λTS is that captureavoiding substitution in the object language is represented by βreduction in the meta language. However, to reason about the metatheory of (simultaneous) substitutions, it may seem that λTS gets in the way: not only does iterated βreduction not capture simultaneity, but also βredexes are not firstclass constructs. This paper proposes a representation of (simultaneous) substitutions in the twolevel logic approach (2LLA), where properties of a specification language are established in a strong reasoning metalogic that supports inductive reasoning. A substitution, which is a partial map from variables to terms, is represented in a form similar to typing contexts, which are partial maps from variables to types; both are firstclass in 2LLA. The standard typing rules for substitutions are then just a kind of context relation that are already wellknown in 2LLA. This representation neither changes the reasoning kernel, nor requires any modification of existing type systems, and does not sacrifice any expressivity. @InProceedings{CPP18p280, author = {Kaustuv Chaudhuri}, title = {A TwoLevel Logic Perspective on (Simultaneous) Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {280292}, doi = {10.1145/3167093}, year = {2018}, } Publisher's Version Info 

Divasón, Jose 
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann , and Akihisa Yamada (University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan) Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^{n} for a fixed nonnegative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a nontrivial case study for these Isabelle tools. @InProceedings{CPP18p2, author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada}, title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213}, doi = {10.1145/3167103}, year = {2018}, } Publisher's Version 

Djalal, Boris 
CPP '18: "A Constructive Formalisation ..."
A Constructive Formalisation of Semialgebraic Sets and Functions
Boris Djalal (Inria, France) Semialgebraic sets and semialgebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semialgebraic sets and functions using embedded firstorder formulae over the language of real closed fields, and we prove the correctness of their geometrical interpretation. In doing so, we exploit a previous formalisation of quantifier elimination on such embedded formulae to guarantee the decidability of several firstorder properties and keep our development constructive. We also exploit it to formalise formulae substitution without having to handle bound variables. @InProceedings{CPP18p240, author = {Boris Djalal}, title = {A Constructive Formalisation of Semialgebraic Sets and Functions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {240251}, doi = {10.1145/3167099}, year = {2018}, } Publisher's Version 

Doczkal, Christian 
CPP '18: "Completeness and Decidability ..."
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal and Joachim Bard (University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Saarland University, Germany) The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are nonconstructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof by Kozen and Parikh into our constructive setting. We base our proof on a Prattstyle decision method for satisfiability constructing finite models for satisfiable formulas and pruning refutations for unsatisfiable formulas. Completeness of Segerberg's axiomatization of PDL is then obtained by translating pruning refutations to derivations in the Hilbert system. We first treat PDL without converse and then extend the proofs to Converse PDL. All results are formalized in Coq/Ssreflect. @InProceedings{CPP18p42, author = {Christian Doczkal and Joachim Bard}, title = {Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {4252}, doi = {10.1145/3167088}, year = {2018}, } Publisher's Version 

Férée, Hugo 
CPP '18: "Formal Proof of PolynomialTime ..."
Formal Proof of PolynomialTime Complexity with QuasiInterpretations
Hugo Férée, Samuel Hym, Micaela Mayero, JeanYves Moyen, and David Nowak (University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France) We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasiinterpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation. @InProceedings{CPP18p146, author = {Hugo Férée and Samuel Hym and Micaela Mayero and JeanYves Moyen and David Nowak}, title = {Formal Proof of PolynomialTime Complexity with QuasiInterpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {146157}, doi = {10.1145/3167097}, year = {2018}, } Publisher's Version Info 

Firsov, Denis 
CPP '18: "Generic Derivation of Induction ..."
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump (University of Iowa, USA) This paper presents generic derivations of induction for impredicatively typed lambdaencoded datatypes, in the Cedille type theory. Cedille is a pure type theory extending the Currystyle Calculus of Constructions with implicit products, primitive heterogeneous equality, and dependent intersections. All data erase to pure lambda terms, and there is no builtin notion of datatype. The derivations are generic in the sense that we derive induction for any datatype which arises as the least fixed point of a signature functor. We consider Churchstyle and Mendlerstyle lambdaencodings. Moreover, the isomorphism of these encodings is proved. Also, we formalize Lambek's lemma as a consequence of expected laws of cancellation, reflection, and fusion. @InProceedings{CPP18p215, author = {Denis Firsov and Aaron Stump}, title = {Generic Derivation of Induction for Impredicative Encodings in Cedille}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {215227}, doi = {10.1145/3167087}, year = {2018}, } Publisher's Version 

Fleury, Mathias 
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich (Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA) Based on our earlier formalization of conflictdriven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further. @InProceedings{CPP18p158, author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich}, title = {A Verified SAT Solver with Watched Literals Using Imperative HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {158171}, doi = {10.1145/3167080}, year = {2018}, } Publisher's Version 

Fournet, Cédric 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Frumin, Dan 
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers , Léon Gondelman, and Niels van der Weide (Radboud University Nijmegen, Netherlands) We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of ”finite sets over type A” à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition. On the foundational side, we use K to define the notions of ”Kuratowskifinite type” and ”Kuratowskifinite subobject”, which we contrast with established notions, e.g. Bishopfinite types and enumerated types. We argue that Kuratowskifiniteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects. From the computational perspective, we show how to use K(A) for an abstract interface for wellknown finite set implementations such as tree and listlike data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A). @InProceedings{CPP18p201, author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide}, title = {Finite Sets in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {201214}, doi = {10.1145/3167085}, year = {2018}, } Publisher's Version Info 

Geuvers, Herman 
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers , Léon Gondelman, and Niels van der Weide (Radboud University Nijmegen, Netherlands) We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of ”finite sets over type A” à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition. On the foundational side, we use K to define the notions of ”Kuratowskifinite type” and ”Kuratowskifinite subobject”, which we contrast with established notions, e.g. Bishopfinite types and enumerated types. We argue that Kuratowskifiniteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects. From the computational perspective, we show how to use K(A) for an abstract interface for wellknown finite set implementations such as tree and listlike data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A). @InProceedings{CPP18p201, author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide}, title = {Finite Sets in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {201214}, doi = {10.1145/3167085}, year = {2018}, } Publisher's Version Info 

Gondelman, Léon 
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers , Léon Gondelman, and Niels van der Weide (Radboud University Nijmegen, Netherlands) We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of ”finite sets over type A” à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition. On the foundational side, we use K to define the notions of ”Kuratowskifinite type” and ”Kuratowskifinite subobject”, which we contrast with established notions, e.g. Bishopfinite types and enumerated types. We argue that Kuratowskifiniteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects. From the computational perspective, we show how to use K(A) for an abstract interface for wellknown finite set implementations such as tree and listlike data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A). @InProceedings{CPP18p201, author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide}, title = {Finite Sets in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {201214}, doi = {10.1145/3167085}, year = {2018}, } Publisher's Version Info 

GrahamLengrand, Stéphane 
CPP '18: "Proofs in ConflictDriven ..."
Proofs in ConflictDriven Theory Combination
Maria Paola Bonacina, Stéphane GrahamLengrand, and Natarajan Shankar (University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA) Searchbased satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflictdriven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (ConflictDriven SATisfiability) is a method for conflictdriven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflictdriven SMTsolving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction. @InProceedings{CPP18p186, author = {Maria Paola Bonacina and Stéphane GrahamLengrand and Natarajan Shankar}, title = {Proofs in ConflictDriven Theory Combination}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {186200}, doi = {10.1145/3167096}, year = {2018}, } Publisher's Version 

Grimm, Niklas 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Grossman, Dan 
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock , and Dan Grossman (University of Washington, USA) Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicated process that is in the trusted computing base (TCB). This paper presents Œuf, a verified compiler from a subset of Gallina to assembly. Œuf’s correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how Œuf’s specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, Œufmaintains a small TCB for its frontend by reflecting Gallina programs to Œufsource and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (e.g., lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate Œuf, we compile Appel’s SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified sha256sum implementation with a small TCB. @InProceedings{CPP18p172, author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman}, title = {Œuf: Minimizing the Coq Extraction TCB}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {172185}, doi = {10.1145/3167089}, year = {2018}, } Publisher's Version CPP '18: "Adapting Proof Automation ..." Adapting Proof Automation to Adapt Proofs Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman (University of Washington, USA; Halfaya Research, USA) We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proofofconcept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling. @InProceedings{CPP18p115, author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman}, title = {Adapting Proof Automation to Adapt Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {115129}, doi = {10.1145/3167094}, year = {2018}, } Publisher's Version 

Hriţcu, Cătălin 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Hym, Samuel 
CPP '18: "Formal Proof of PolynomialTime ..."
Formal Proof of PolynomialTime Complexity with QuasiInterpretations
Hugo Férée, Samuel Hym, Micaela Mayero, JeanYves Moyen, and David Nowak (University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France) We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasiinterpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation. @InProceedings{CPP18p146, author = {Hugo Férée and Samuel Hym and Micaela Mayero and JeanYves Moyen and David Nowak}, title = {Formal Proof of PolynomialTime Complexity with QuasiInterpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {146157}, doi = {10.1145/3167097}, year = {2018}, } Publisher's Version Info 

Joosten, Sebastiaan 
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann , and Akihisa Yamada (University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan) Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^{n} for a fixed nonnegative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a nontrivial case study for these Isabelle tools. @InProceedings{CPP18p2, author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada}, title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213}, doi = {10.1145/3167103}, year = {2018}, } Publisher's Version 

Kaiser, Jonas 
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over WellScoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark (Saarland University, Germany) The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiationcompatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems. With our framework we define variable renaming and instantiation, syntax directed typing and certain unary logical relations for System F. These definitons lead to concise proofs of type preservation, as well as weak and strong normalisation. Our framework is designed to serve as the theoretical foundation of future versions of the Autosubst Coq library. All developments and case studies are formalised in the Coq proof assistant. @InProceedings{CPP18p293, author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark}, title = {Binder Aware Recursion over WellScoped de Bruijn Syntax}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {293306}, doi = {10.1145/3167098}, year = {2018}, } Publisher's Version Info 

Kaliszyk, Cezary 
CPP '18: "Formal Microeconomic Foundations ..."
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert (University of Innsbruck, Austria) Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic actors are consumers, as well as a version of the ArrowDebreu Model, a private ownership economy, which includes production facilities. Interestingly, the definitions of various components of the economic models differ in the economic literature. We therefore show the equivalences and implications between various presentations, which allows us to create an extensible foundation for formalizing microeconomics and game theory compatible with multiple economic theories. We prove the First Theorem of Welfare Economics in both economic models. The theorem is the mathematical formulation of Adam Smith’s famous invisible hand and states that a group of selfinterested and rational actors will eventually achieve an efficient allocation of goods. The formal proofs allow us to find more precise assumptions than those found in the economic literature. @InProceedings{CPP18p91, author = {Cezary Kaliszyk and Julian Parsert}, title = {Formal Microeconomic Foundations and the First Welfare Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91101}, doi = {10.1145/3167100}, year = {2018}, } Publisher's Version 

Kirst, Dominik 
CPP '18: "Large Model Constructions ..."
Large Model Constructions for SecondOrder ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka (Saarland University, Germany) We study various models of classical secondorder set theories in the dependent type theory of Coq. Without logical assumptions, Aczel’s setsastrees interpretation yields an intensional model of secondorder ZF with functional replacement. Building on work of Werner and Barras, we discuss the need for quotient axioms in order to obtain extensional models with relational replacement and to construct large sets. Specifically, we show that the consistency strength of Coq extended by excluded middle and a description operator on wellfounded trees allows for constructing models with exactly n Grothendieck universes for every natural number n. By a previous categoricity result based on Zermelo’s embedding theorem, it follows that those models are unique up to isomorphism. Moreover, we show that the smallest universe contains exactly the hereditarily finite sets and give a concise independence proof of the foundation axiom based on permutation models. @InProceedings{CPP18p228, author = {Dominik Kirst and Gert Smolka}, title = {Large Model Constructions for SecondOrder ZF in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {228239}, doi = {10.1145/3167095}, year = {2018}, } Publisher's Version Info 

Kunčar, Ondřej 
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann , and Akihisa Yamada (University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan) Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^{n} for a fixed nonnegative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a nontrivial case study for these Isabelle tools. @InProceedings{CPP18p2, author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada}, title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213}, doi = {10.1145/3167103}, year = {2018}, } Publisher's Version 

Lammich, Peter 
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich (Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA) Based on our earlier formalization of conflictdriven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further. @InProceedings{CPP18p158, author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich}, title = {A Verified SAT Solver with Watched Literals Using Imperative HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {158171}, doi = {10.1145/3167080}, year = {2018}, } Publisher's Version 

Lenglet, Sergueï 
CPP '18: "HOπ in Coq ..."
HOπ in Coq
Sergueï Lenglet and Alan Schmitt (University of Lorraine, France; Inria, France) We propose a formalization of HOπ in Coq, a process calculus where messages carry processes. Such a higherorder calculus features two very different kinds of binder: process input, similar to λabstraction, and name restriction, whose scope can be expanded by communication. We formalize strong context bisimilarity and prove it is compatible, i.e., closed under every context, using Howe’s method, based on several proof schemes we developed in a previous paper. @InProceedings{CPP18p252, author = {Sergueï Lenglet and Alan Schmitt}, title = {HOπ in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {252265}, doi = {10.1145/3167083}, year = {2018}, } Publisher's Version 

Leo, John 
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman (University of Washington, USA; Halfaya Research, USA) We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proofofconcept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling. @InProceedings{CPP18p115, author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman}, title = {Adapting Proof Automation to Adapt Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {115129}, doi = {10.1145/3167094}, year = {2018}, } Publisher's Version 

Maffei, Matteo 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Maillard, Kenji 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Mayero, Micaela 
CPP '18: "Formal Proof of PolynomialTime ..."
Formal Proof of PolynomialTime Complexity with QuasiInterpretations
Hugo Férée, Samuel Hym, Micaela Mayero, JeanYves Moyen, and David Nowak (University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France) We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasiinterpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation. @InProceedings{CPP18p146, author = {Hugo Férée and Samuel Hym and Micaela Mayero and JeanYves Moyen and David Nowak}, title = {Formal Proof of PolynomialTime Complexity with QuasiInterpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {146157}, doi = {10.1145/3167097}, year = {2018}, } Publisher's Version Info 

McKinna, James 
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark (University of Edinburgh, UK) The idea of a context lemma spans a range of programminglanguage models: from Milner’s original through the CIU theorem to ‘CIUlike’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some restricted class of contexts: applicative, evaluation, reduction, etc. We formally reconstruct a distinctive proof method for context lemmas based on cyclic inclusion of three program approximations: by triangulating between ‘applicative’ and ‘logical’ relations we prove that both match the observational notion, while being simpler to compute. Moreover, the observational component of the triangle condenses a series of approximations covering variation in the literature around what variablecapturing structure qualifies as a ‘context’. Although entirely concrete, our approach involves no term dissection or inspection of reduction sequences; instead we draw on previous context lemmas using operational logical relations and biorthogonality. We demonstrate the method for a finegrained callbyvalue presentation of the simplytyped lambdacalculus, and extend to a CIU result formulated with frame stacks. All this is formalised and proved in Agda: building on work of Allais et al., we exploit dependent types to specify lambdacalculus terms as welltyped and wellscoped by construction. By doing so, we seek to dispel any lingering anxieties about the manipulation of concrete contexts when reasoning about bound variables, capturing substitution, and observational equivalences. @InProceedings{CPP18p102, author = {Craig McLaughlin and James McKinna and Ian Stark}, title = {Triangulating Context Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102114}, doi = {10.1145/3167081}, year = {2018}, } Publisher's Version 

McLaughlin, Craig 
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark (University of Edinburgh, UK) The idea of a context lemma spans a range of programminglanguage models: from Milner’s original through the CIU theorem to ‘CIUlike’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some restricted class of contexts: applicative, evaluation, reduction, etc. We formally reconstruct a distinctive proof method for context lemmas based on cyclic inclusion of three program approximations: by triangulating between ‘applicative’ and ‘logical’ relations we prove that both match the observational notion, while being simpler to compute. Moreover, the observational component of the triangle condenses a series of approximations covering variation in the literature around what variablecapturing structure qualifies as a ‘context’. Although entirely concrete, our approach involves no term dissection or inspection of reduction sequences; instead we draw on previous context lemmas using operational logical relations and biorthogonality. We demonstrate the method for a finegrained callbyvalue presentation of the simplytyped lambdacalculus, and extend to a CIU result formulated with frame stacks. All this is formalised and proved in Agda: building on work of Allais et al., we exploit dependent types to specify lambdacalculus terms as welltyped and wellscoped by construction. By doing so, we seek to dispel any lingering anxieties about the manipulation of concrete contexts when reasoning about bound variables, capturing substitution, and observational equivalences. @InProceedings{CPP18p102, author = {Craig McLaughlin and James McKinna and Ian Stark}, title = {Triangulating Context Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102114}, doi = {10.1145/3167081}, year = {2018}, } Publisher's Version 

Moyen, JeanYves 
CPP '18: "Formal Proof of PolynomialTime ..."
Formal Proof of PolynomialTime Complexity with QuasiInterpretations
Hugo Férée, Samuel Hym, Micaela Mayero, JeanYves Moyen, and David Nowak (University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France) We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasiinterpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation. @InProceedings{CPP18p146, author = {Hugo Férée and Samuel Hym and Micaela Mayero and JeanYves Moyen and David Nowak}, title = {Formal Proof of PolynomialTime Complexity with QuasiInterpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {146157}, doi = {10.1145/3167097}, year = {2018}, } Publisher's Version Info 

Mullen, Eric 
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock , and Dan Grossman (University of Washington, USA) Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicated process that is in the trusted computing base (TCB). This paper presents Œuf, a verified compiler from a subset of Gallina to assembly. Œuf’s correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how Œuf’s specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, Œufmaintains a small TCB for its frontend by reflecting Gallina programs to Œufsource and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (e.g., lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate Œuf, we compile Appel’s SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified sha256sum implementation with a small TCB. @InProceedings{CPP18p172, author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman}, title = {Œuf: Minimizing the Coq Extraction TCB}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {172185}, doi = {10.1145/3167089}, year = {2018}, } Publisher's Version 

Nowak, David 
CPP '18: "Formal Proof of PolynomialTime ..."
Formal Proof of PolynomialTime Complexity with QuasiInterpretations
Hugo Férée, Samuel Hym, Micaela Mayero, JeanYves Moyen, and David Nowak (University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France) We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasiinterpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation. @InProceedings{CPP18p146, author = {Hugo Férée and Samuel Hym and Micaela Mayero and JeanYves Moyen and David Nowak}, title = {Formal Proof of PolynomialTime Complexity with QuasiInterpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {146157}, doi = {10.1145/3167097}, year = {2018}, } Publisher's Version Info 

Parsert, Julian 
CPP '18: "Formal Microeconomic Foundations ..."
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert (University of Innsbruck, Austria) Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic actors are consumers, as well as a version of the ArrowDebreu Model, a private ownership economy, which includes production facilities. Interestingly, the definitions of various components of the economic models differ in the economic literature. We therefore show the equivalences and implications between various presentations, which allows us to create an extensible foundation for formalizing microeconomics and game theory compatible with multiple economic theories. We prove the First Theorem of Welfare Economics in both economic models. The theorem is the mathematical formulation of Adam Smith’s famous invisible hand and states that a group of selfinterested and rational actors will eventually achieve an efficient allocation of goods. The formal proofs allow us to find more precise assumptions than those found in the economic literature. @InProceedings{CPP18p91, author = {Cezary Kaliszyk and Julian Parsert}, title = {Formal Microeconomic Foundations and the First Welfare Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91101}, doi = {10.1145/3167100}, year = {2018}, } Publisher's Version 

Pernsteiner, Stuart 
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock , and Dan Grossman (University of Washington, USA) Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicated process that is in the trusted computing base (TCB). This paper presents Œuf, a verified compiler from a subset of Gallina to assembly. Œuf’s correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how Œuf’s specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, Œufmaintains a small TCB for its frontend by reflecting Gallina programs to Œufsource and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (e.g., lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate Œuf, we compile Appel’s SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified sha256sum implementation with a small TCB. @InProceedings{CPP18p172, author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman}, title = {Œuf: Minimizing the Coq Extraction TCB}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {172185}, doi = {10.1145/3167089}, year = {2018}, } Publisher's Version 

Pientka, Brigitte 
CPP '18: "POPLMark Reloaded: Mechanizing ..."
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka (McGill University, Canada) Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. Over the past decade, the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming languages. Focusing on the the metatheory of System F with subtyping, it allowed the programming languages community to survey existing techniques to represent and reason about syntactic structures with binders and promote the use of proof assistants. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers. As a followup to the POPLMark Challenge, we propose a new collection of benchmarks that use proofs by logical relations. Such proofs are now used to attack problems in the theory of complex languages models, with applications to issues in equivalence of programs, compiler correctness, representation independence and even more intensional properties such as noninterference, differential privacy and secure multilanguage interoperability. Yet, they remain challenging to mechanize. In this talk, we focus on one particular challenge problem, namely strong normalization of a simplytyped lambdacalculus with a proof by Kripkestyle logical relations. We will advocate a modern view of this wellunderstood problem by formulating our logical relation on welltyped terms. Using this case study, we share some of the lessons learned tackling this challenge problem in Beluga, a proof environment that supports higherorder abstract syntax encodings, firstclass context and firstclass substitutions. We also discuss and highlight similarities, strategies, and limitations in other proof assistants when tackling this challenge problem. We hope others will be motivated to submit solutions! The goal of this talk is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses. @InProceedings{CPP18p1, author = {Brigitte Pientka}, title = {POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {11}, doi = {10.1145/3167102}, year = {2018}, } Publisher's Version 

Pîrlea, George 
CPP '18: "Mechanising Blockchain Consensus ..."
Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey (University College London, UK) We present the first formalisation of a blockchainbased distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant. Our development includes a reference mechanisation of the block forest data structure, necessary for implementing provably correct pernode protocol logic. We also define a model of a network, implementing the protocol in the form of a replicated statetransition system. The protocol's executions are modeled via a smallstep operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated. In this work, we focus on the notion of global system safety, proving a form of eventual consistency. To do so, we provide a library of theorems about a pure functional implementation of block forests, define an inductive system invariant, and show that, in a quiescent system state, it implies a global agreement on the state of pernode transaction ledgers. Our development is parametric with respect to implementations of several security primitives, such as hashfunctions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy. All results described in this paper are formalised in Coq. @InProceedings{CPP18p78, author = {George Pîrlea and Ilya Sergey}, title = {Mechanising Blockchain Consensus}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7890}, doi = {10.1145/3167086}, year = {2018}, } Publisher's Version Info 

Protzenko, Jonathan 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Ramananandro, Tahina 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Rastogi, Aseem 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Ringer, Talia 
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman (University of Washington, USA; Halfaya Research, USA) We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proofofconcept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling. @InProceedings{CPP18p115, author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman}, title = {Adapting Proof Automation to Adapt Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {115129}, doi = {10.1145/3167094}, year = {2018}, } Publisher's Version 

Rizkallah, Christine 
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal SpectorZabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich (University of Pennsylvania, USA) We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hstocoq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies – a lawful Monad instance, “Hutton’s razor”, and an existing data structure library – and prove their correctness. These examples show that this approach is viable: both that hstocoq applies to existing Haskell code, and that the output it produces is amenable to verification. @InProceedings{CPP18p14, author = {Antal SpectorZabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich}, title = {Total Haskell is Reasonable Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1427}, doi = {10.1145/3167092}, year = {2018}, } Publisher's Version Info 

Rouhling, Damien 
CPP '18: "A Formal Proof in Coq of a ..."
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling (University of Côte d'Azur, France; Inria, France) Control theory provides techniques to design controllers, or control functions, for dynamical systems with inputs, so as to grant a particular behaviour of such a system. The inverted pendulum is a classic system in control theory: it is used as a benchmark for nonlinear control techniques and is a model for several other systems with various applications. We formalized in the Coq proof assistant the proof of soundness of a control function for the inverted pendulum. This is a first step towards the formal verification of more complex systems for which safety may be critical. @InProceedings{CPP18p28, author = {Damien Rouhling}, title = {A Formal Proof in Coq of a Control Function for the Inverted Pendulum}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {2841}, doi = {10.1145/3167101}, year = {2018}, } Publisher's Version 

Schäfer, Steven 
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over WellScoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark (Saarland University, Germany) The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiationcompatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems. With our framework we define variable renaming and instantiation, syntax directed typing and certain unary logical relations for System F. These definitons lead to concise proofs of type preservation, as well as weak and strong normalisation. Our framework is designed to serve as the theoretical foundation of future versions of the Autosubst Coq library. All developments and case studies are formalised in the Coq proof assistant. @InProceedings{CPP18p293, author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark}, title = {Binder Aware Recursion over WellScoped de Bruijn Syntax}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {293306}, doi = {10.1145/3167098}, year = {2018}, } Publisher's Version Info 

Schmitt, Alan 
CPP '18: "HOπ in Coq ..."
HOπ in Coq
Sergueï Lenglet and Alan Schmitt (University of Lorraine, France; Inria, France) We propose a formalization of HOπ in Coq, a process calculus where messages carry processes. Such a higherorder calculus features two very different kinds of binder: process input, similar to λabstraction, and name restriction, whose scope can be expanded by communication. We formalize strong context bisimilarity and prove it is compatible, i.e., closed under every context, using Howe’s method, based on several proof schemes we developed in a previous paper. @InProceedings{CPP18p252, author = {Sergueï Lenglet and Alan Schmitt}, title = {HOπ in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {252265}, doi = {10.1145/3167083}, year = {2018}, } Publisher's Version 

Sergey, Ilya 
CPP '18: "Mechanising Blockchain Consensus ..."
Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey (University College London, UK) We present the first formalisation of a blockchainbased distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant. Our development includes a reference mechanisation of the block forest data structure, necessary for implementing provably correct pernode protocol logic. We also define a model of a network, implementing the protocol in the form of a replicated statetransition system. The protocol's executions are modeled via a smallstep operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated. In this work, we focus on the notion of global system safety, proving a form of eventual consistency. To do so, we provide a library of theorems about a pure functional implementation of block forests, define an inductive system invariant, and show that, in a quiescent system state, it implies a global agreement on the state of pernode transaction ledgers. Our development is parametric with respect to implementations of several security primitives, such as hashfunctions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy. All results described in this paper are formalised in Coq. @InProceedings{CPP18p78, author = {George Pîrlea and Ilya Sergey}, title = {Mechanising Blockchain Consensus}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {7890}, doi = {10.1145/3167086}, year = {2018}, } Publisher's Version Info 

Shankar, Natarajan 
CPP '18: "Proofs in ConflictDriven ..."
Proofs in ConflictDriven Theory Combination
Maria Paola Bonacina, Stéphane GrahamLengrand, and Natarajan Shankar (University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA) Searchbased satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflictdriven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (ConflictDriven SATisfiability) is a method for conflictdriven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflictdriven SMTsolving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction. @InProceedings{CPP18p186, author = {Maria Paola Bonacina and Stéphane GrahamLengrand and Natarajan Shankar}, title = {Proofs in ConflictDriven Theory Combination}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {186200}, doi = {10.1145/3167096}, year = {2018}, } Publisher's Version 

Smolka, Gert 
CPP '18: "Large Model Constructions ..."
Large Model Constructions for SecondOrder ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka (Saarland University, Germany) We study various models of classical secondorder set theories in the dependent type theory of Coq. Without logical assumptions, Aczel’s setsastrees interpretation yields an intensional model of secondorder ZF with functional replacement. Building on work of Werner and Barras, we discuss the need for quotient axioms in order to obtain extensional models with relational replacement and to construct large sets. Specifically, we show that the consistency strength of Coq extended by excluded middle and a description operator on wellfounded trees allows for constructing models with exactly n Grothendieck universes for every natural number n. By a previous categoricity result based on Zermelo’s embedding theorem, it follows that those models are unique up to isomorphism. Moreover, we show that the smallest universe contains exactly the hereditarily finite sets and give a concise independence proof of the foundation axiom based on permutation models. @InProceedings{CPP18p228, author = {Dominik Kirst and Gert Smolka}, title = {Large Model Constructions for SecondOrder ZF in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {228239}, doi = {10.1145/3167095}, year = {2018}, } Publisher's Version Info 

SpectorZabusky, Antal 
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal SpectorZabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich (University of Pennsylvania, USA) We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hstocoq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies – a lawful Monad instance, “Hutton’s razor”, and an existing data structure library – and prove their correctness. These examples show that this approach is viable: both that hstocoq applies to existing Haskell code, and that the output it produces is amenable to verification. @InProceedings{CPP18p14, author = {Antal SpectorZabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich}, title = {Total Haskell is Reasonable Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1427}, doi = {10.1145/3167092}, year = {2018}, } Publisher's Version Info 

Staples, Mark 
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples (Data61 at CSIRO, Australia; ENS ParisSaclay, France; University of ParisSaclay, France; UNSW, Australia) Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety, security, or missioncritical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straightline code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts. @InProceedings{CPP18p66, author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples}, title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {6677}, doi = {10.1145/3167084}, year = {2018}, } Publisher's Version 

Stark, Ian 
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark (University of Edinburgh, UK) The idea of a context lemma spans a range of programminglanguage models: from Milner’s original through the CIU theorem to ‘CIUlike’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some restricted class of contexts: applicative, evaluation, reduction, etc. We formally reconstruct a distinctive proof method for context lemmas based on cyclic inclusion of three program approximations: by triangulating between ‘applicative’ and ‘logical’ relations we prove that both match the observational notion, while being simpler to compute. Moreover, the observational component of the triangle condenses a series of approximations covering variation in the literature around what variablecapturing structure qualifies as a ‘context’. Although entirely concrete, our approach involves no term dissection or inspection of reduction sequences; instead we draw on previous context lemmas using operational logical relations and biorthogonality. We demonstrate the method for a finegrained callbyvalue presentation of the simplytyped lambdacalculus, and extend to a CIU result formulated with frame stacks. All this is formalised and proved in Agda: building on work of Allais et al., we exploit dependent types to specify lambdacalculus terms as welltyped and wellscoped by construction. By doing so, we seek to dispel any lingering anxieties about the manipulation of concrete contexts when reasoning about bound variables, capturing substitution, and observational equivalences. @InProceedings{CPP18p102, author = {Craig McLaughlin and James McKinna and Ian Stark}, title = {Triangulating Context Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {102114}, doi = {10.1145/3167081}, year = {2018}, } Publisher's Version 

Stark, Kathrin 
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over WellScoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark (Saarland University, Germany) The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiationcompatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems. With our framework we define variable renaming and instantiation, syntax directed typing and certain unary logical relations for System F. These definitons lead to concise proofs of type preservation, as well as weak and strong normalisation. Our framework is designed to serve as the theoretical foundation of future versions of the Autosubst Coq library. All developments and case studies are formalised in the Coq proof assistant. @InProceedings{CPP18p293, author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark}, title = {Binder Aware Recursion over WellScoped de Bruijn Syntax}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {293306}, doi = {10.1145/3167098}, year = {2018}, } Publisher's Version Info 

Stump, Aaron 
CPP '18: "Generic Derivation of Induction ..."
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump (University of Iowa, USA) This paper presents generic derivations of induction for impredicatively typed lambdaencoded datatypes, in the Cedille type theory. Cedille is a pure type theory extending the Currystyle Calculus of Constructions with implicit products, primitive heterogeneous equality, and dependent intersections. All data erase to pure lambda terms, and there is no builtin notion of datatype. The derivations are generic in the sense that we derive induction for any datatype which arises as the least fixed point of a signature functor. We consider Churchstyle and Mendlerstyle lambdaencodings. Moreover, the isomorphism of these encodings is proved. Also, we formalize Lambek's lemma as a consequence of expected laws of cancellation, reflection, and fusion. @InProceedings{CPP18p215, author = {Denis Firsov and Aaron Stump}, title = {Generic Derivation of Induction for Impredicative Encodings in Cedille}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {215227}, doi = {10.1145/3167087}, year = {2018}, } Publisher's Version 

Swamy, Nikhil 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 

Tatlock, Zachary 
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock , and Dan Grossman (University of Washington, USA) Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicated process that is in the trusted computing base (TCB). This paper presents Œuf, a verified compiler from a subset of Gallina to assembly. Œuf’s correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how Œuf’s specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, Œufmaintains a small TCB for its frontend by reflecting Gallina programs to Œufsource and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (e.g., lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate Œuf, we compile Appel’s SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified sha256sum implementation with a small TCB. @InProceedings{CPP18p172, author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman}, title = {Œuf: Minimizing the Coq Extraction TCB}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {172185}, doi = {10.1145/3167089}, year = {2018}, } Publisher's Version 

Thiemann, René 
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann , and Akihisa Yamada (University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan) Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^{n} for a fixed nonnegative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a nontrivial case study for these Isabelle tools. @InProceedings{CPP18p2, author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada}, title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213}, doi = {10.1145/3167103}, year = {2018}, } Publisher's Version 

Watt, Conrad 
CPP '18: "Mechanising and Verifying ..."
Mechanising and Verifying the WebAssembly Specification
Conrad Watt (University of Cambridge, UK) WebAssembly is a new lowlevel language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js and Native Client. The WebAssembly working group has incorporated formal techniques into the development of the language, but their efforts so far have focussed on pen and paper formal specification. We present a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker. Moreover, we present a fully mechanised proof of the soundness of the WebAssembly type system, and detail how our work on this proof has exposed several issues with the official WebAssembly specification, influencing its development. Finally, we give a brief account of our efforts in performing differential fuzzing of our interpreter against industry implementations. @InProceedings{CPP18p53, author = {Conrad Watt}, title = {Mechanising and Verifying the WebAssembly Specification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {5365}, doi = {10.1145/3167082}, year = {2018}, } Publisher's Version 

Weide, Niels van der 
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers , Léon Gondelman, and Niels van der Weide (Radboud University Nijmegen, Netherlands) We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of ”finite sets over type A” à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition. On the foundational side, we use K to define the notions of ”Kuratowskifinite type” and ”Kuratowskifinite subobject”, which we contrast with established notions, e.g. Bishopfinite types and enumerated types. We argue that Kuratowskifiniteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects. From the computational perspective, we show how to use K(A) for an abstract interface for wellknown finite set implementations such as tree and listlike data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A). @InProceedings{CPP18p201, author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide}, title = {Finite Sets in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {201214}, doi = {10.1145/3167085}, year = {2018}, } Publisher's Version Info 

Weirich, Stephanie 
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal SpectorZabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich (University of Pennsylvania, USA) We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hstocoq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies – a lawful Monad instance, “Hutton’s razor”, and an existing data structure library – and prove their correctness. These examples show that this approach is viable: both that hstocoq applies to existing Haskell code, and that the output it produces is amenable to verification. @InProceedings{CPP18p14, author = {Antal SpectorZabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich}, title = {Total Haskell is Reasonable Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1427}, doi = {10.1145/3167092}, year = {2018}, } Publisher's Version Info 

Wieczorek, Paweł 
CPP '18: "A Coq Formalization of Normalization ..."
A Coq Formalization of Normalization by Evaluation for MartinLöf Type Theory
Paweł Wieczorek and Dariusz Biernacki (University of Wrocław, Poland) We present a Coq formalization of the normalizationbyevaluation algorithm for MartinLöf dependent type theory with one universe and judgmental equality. The end results of the formalization are certified implementations of a reductionfree normalizer and of a decision procedure for term equality. The formalization takes advantage of a graphbased variant of the BoveCapretta method to encode mutually recursive evaluation functions with nested recursive calls. The proof of completeness, which uses the PERmodel of dependent types, is formalized by relying on impredicativity of the Coq system rather than on the commonly used inductionrecursion scheme which is not available in Coq. The proof of soundness is formalized by encoding logical relations as partial functions. @InProceedings{CPP18p266, author = {Paweł Wieczorek and Dariusz Biernacki}, title = {A Coq Formalization of Normalization by Evaluation for MartinLöf Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {266279}, doi = {10.1145/3167091}, year = {2018}, } Publisher's Version Info 

Wilcox, James R. 
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock , and Dan Grossman (University of Washington, USA) Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicated process that is in the trusted computing base (TCB). This paper presents Œuf, a verified compiler from a subset of Gallina to assembly. Œuf’s correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how Œuf’s specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, Œufmaintains a small TCB for its frontend by reflecting Gallina programs to Œufsource and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (e.g., lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate Œuf, we compile Appel’s SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified sha256sum implementation with a small TCB. @InProceedings{CPP18p172, author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman}, title = {Œuf: Minimizing the Coq Extraction TCB}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {172185}, doi = {10.1145/3167089}, year = {2018}, } Publisher's Version 

Yamada, Akihisa 
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann , and Akihisa Yamada (University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan) Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^{n} for a fixed nonnegative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a nontrivial case study for these Isabelle tools. @InProceedings{CPP18p2, author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada}, title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213}, doi = {10.1145/3167103}, year = {2018}, } Publisher's Version 

Yazdani, Nathaniel 
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman (University of Washington, USA; Halfaya Research, USA) We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proofofconcept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling. @InProceedings{CPP18p115, author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman}, title = {Adapting Proof Automation to Adapt Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {115129}, doi = {10.1145/3167094}, year = {2018}, } Publisher's Version 

ZanellaBéguelin, Santiago 
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard , Cédric Fournet , Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , and Santiago ZanellaBéguelin (Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India) Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and gamebased cryptographic security. By relying on SMTbased automation, unary weakest preconditions, userdefined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. @InProceedings{CPP18p130, author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago ZanellaBéguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {130145}, doi = {10.1145/3167090}, year = {2018}, } Publisher's Version 
71 authors
proc time: 15.93