CPP 2018 – Proceedings

7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), January 8–9, 2018, Los Angeles, CA, USA

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

Frontmatter

Invited Talks

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)
Article: poplws18cppmain-id101-p doi:

Verifing Programs and Systems

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

Publisher's Version Article: poplws18cppmain-id51-p doi:10.1145/3167092

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

Publisher's Version Article: poplws18cppmain-id41-p doi:10.1145/3167101

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)

Publisher's Version Article: poplws18cppmain-id42-p doi:10.1145/3167088

Verified Applications

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

Publisher's Version Article: poplws18cppmain-id13-p doi:10.1145/3167082

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)

Publisher's Version Article: poplws18cppmain-id25-p doi:10.1145/3167084

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

Publisher's Version Article: poplws18cppmain-id48-p doi:10.1145/3167086

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

Publisher's Version Article: poplws18cppmain-id29-p doi:10.1145/3167100

Proof Methods and Libraries

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

Publisher's Version Article: poplws18cppmain-id2-p doi:10.1145/3167081

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

Publisher's Version Article: poplws18cppmain-id23-p doi:10.1145/3167094

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)

Publisher's Version Article: poplws18cppmain-id14-p doi:10.1145/3167090

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)

Publisher's Version Article: poplws18cppmain-id39-p doi:10.1145/3167097

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)

Publisher's Version Article: poplws18cppmain-id7-p doi:10.1145/3167080

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

Publisher's Version Article: poplws18cppmain-id12-p doi:10.1145/3167089

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)

Publisher's Version Article: poplws18cppmain-id32-p doi:10.1145/3167096

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)

Publisher's Version Article: poplws18cppmain-id38-p doi:10.1145/3167085

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

Publisher's Version Article: poplws18cppmain-id8-p doi:10.1145/3167095

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

Publisher's Version Article: poplws18cppmain-id19-p doi:10.1145/3167099

Formalizing Meta-Theory

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

Publisher's Version Article: poplws18cppmain-id18-p doi:10.1145/3167083

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

Publisher's Version Article: poplws18cppmain-id59-p doi:10.1145/3167093

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

Publisher's Version Article: poplws18cppmain-id60-p doi:10.1145/3167098