CPP 2018 – Proceedings

7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)

Frontmatter

Invited Talks

POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka
(McGill University, Canada)


@InProceedings{CPP18p1, author = {Brigitte Pientka}, title = {POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2018}, }

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)


@InProceedings{CPP18p17, 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 = {17-16}, doi = {}, year = {2018}, }

Verifing Programs and Systems

Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)


@InProceedings{CPP18p33, author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich}, title = {Total Haskell is Reasonable Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {33-32}, doi = {}, year = {2018}, }

A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling
(University of Côte d'Azur, France; Inria, France)


@InProceedings{CPP18p49, author = {Damien Rouhling}, title = {A Formal Proof in Coq of a Control Function for the Inverted Pendulum}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {49-48}, doi = {}, year = {2018}, }

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)


@InProceedings{CPP18p65, 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 = {65-64}, doi = {}, year = {2018}, }

Verified Applications

Mechanising and Verifying the WebAssembly Specification
Conrad Watt
(University of Cambridge, UK)


@InProceedings{CPP18p81, author = {Conrad Watt}, title = {Mechanising and Verifying the WebAssembly Specification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {81-80}, doi = {}, year = {2018}, }

Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples
(Data61 at CSIRO, Australia; ENS Paris-Saclay, France; University of Paris-Saclay, France; UNSW, Australia)


@InProceedings{CPP18p97, 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 = {97-96}, doi = {}, year = {2018}, }

Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey
(University College London, UK)


@InProceedings{CPP18p113, author = {George Pîrlea and Ilya Sergey}, title = {Mechanising Blockchain Consensus}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {113-112}, doi = {}, year = {2018}, }

Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert
(University of Innsbruck, Austria)


@InProceedings{CPP18p129, author = {Cezary Kaliszyk and Julian Parsert}, title = {Formal Microeconomic Foundations and the First Welfare Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {129-128}, doi = {}, year = {2018}, }

Proof Methods and Libraries

Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark
(University of Edinburgh, UK)


@InProceedings{CPP18p145, author = {Craig McLaughlin and James McKinna and Ian Stark}, title = {Triangulating Context Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {145-144}, doi = {}, year = {2018}, }

Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)


@InProceedings{CPP18p161, 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 = {161-160}, doi = {}, year = {2018}, }

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 Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)


@InProceedings{CPP18p177, 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 Zanella-Béguelin}, title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {177-176}, doi = {}, year = {2018}, }

Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)


@InProceedings{CPP18p193, author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak}, title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {193-192}, doi = {}, year = {2018}, }

Trusted Verification Frameworks and Systems

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)


@InProceedings{CPP18p209, 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 = {209-208}, doi = {}, year = {2018}, }

Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)


@InProceedings{CPP18p225, 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 = {225-224}, doi = {}, year = {2018}, }

Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar
(University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA)


@InProceedings{CPP18p241, author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan Shankar}, title = {Proofs in Conflict-Driven Theory Combination}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {241-240}, doi = {}, year = {2018}, }

Type Theory, Set Theory, and Formalized Mathematics

Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide
(Radboud University Nijmegen, Netherlands)


@InProceedings{CPP18p257, 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 = {257-256}, doi = {}, year = {2018}, }

Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump
(University of Iowa, USA)


@InProceedings{CPP18p273, author = {Denis Firsov and Aaron Stump}, title = {Generic Derivation of Induction for Impredicative Encodings in Cedille}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {273-272}, doi = {}, year = {2018}, }

Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka
(Saarland University, Germany)


@InProceedings{CPP18p289, author = {Dominik Kirst and Gert Smolka}, title = {Large Model Constructions for Second-Order ZF in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {289-288}, doi = {}, year = {2018}, }

A Constructive Formalisation of Semi-algebraic Sets and Functions
Boris Djalal
(Inria, France)


@InProceedings{CPP18p305, author = {Boris Djalal}, title = {A Constructive Formalisation of Semi-algebraic Sets and Functions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {305-304}, doi = {}, year = {2018}, }

Formalizing Meta-Theory

HOπ in Coq
Sergueï Lenglet and Alan Schmitt
(University of Lorraine, France; Inria, France)


@InProceedings{CPP18p321, author = {Sergueï Lenglet and Alan Schmitt}, title = {HOπ in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {321-320}, doi = {}, year = {2018}, }

A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek and Dariusz Biernacki
(University of Wrocław, Poland)


@InProceedings{CPP18p337, author = {Paweł Wieczorek and Dariusz Biernacki}, title = {A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {337-336}, doi = {}, year = {2018}, }

A Two-Level Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri
(Inria, France; École Polytechnique, France)


@InProceedings{CPP18p353, author = {Kaustuv Chaudhuri}, title = {A Two-Level Logic Perspective on (Simultaneous) Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2018}, }

Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark
(Saarland University, Germany)


@InProceedings{CPP18p369, author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark}, title = {Binder Aware Recursion over Well-Scoped de Bruijn Syntax}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {369-368}, doi = {}, year = {2018}, }

proc time: 0.85