POPL 2018 Co-Located Events
POPL 2018 Co-Located Events
Powered by
Conference Publishing Consulting

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

CPP 2018 – Advance Table of Contents

Contents - Abstracts - Authors

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


Title Page
Welcome from the Chairs

Invited Talks

POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka
(McGill University, Canada)
Article Search
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 Search

Verifing Programs and Systems

Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)
Article Search Info
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling
(University of Côte d'Azur, France; Inria, France)
Article Search
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)
Article Search Archive submitted (0 MB) Artifacts Available

Verified Applications

Mechanising and Verifying the WebAssembly Specification
Conrad Watt
(University of Cambridge, UK)
Article Search
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)
Article Search
Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey
(University College London, UK)
Preprint Archive submitted (0 MB) Info Artifacts Available
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert
(University of Innsbruck, Austria)
Article Search

Proof Methods and Libraries

Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark
(University of Edinburgh, UK)
Article Search
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)
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)
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)
Article Search Info

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)
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
Article Search
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)
Article Search

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)
Article Search Archive submitted (0 MB) Info Artifacts Available
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump
(University of Iowa, USA)
Article Search
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka
(Saarland University, Germany)
Article Search Info
A Constructive Formalisation of Semi-algebraic Sets and Functions
Boris Djalal
(Inria, France)
Article Search

Formalizing Meta-Theory

HOπ in Coq
Sergueï Lenglet and Alan Schmitt
(University of Lorraine, France; Inria, France)
Article Search
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek and Dariusz Biernacki
(University of Wrocław, Poland)
Article Search Archive submitted (0 MB) Info Artifacts Available
A Two-Level Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri
(Inria, France; École Polytechnique, France)
Preprint Archive submitted (0 MB) Info Artifacts Available
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark
(Saarland University, Germany)
Article Search Info

proc time: 0.09