CPP 2020 – Proceedings

9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)

Frontmatter

Invited Talks

Matching Logic: The Foundation of the K Framework (Invited Talk)
Grigore Roşu and Xiaohong Chen
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)

Publisher's Version

Proof Assistants at the Hardware-Software Interface (Invited Talk)
Adam Chlipala
(Massachusetts Institute of Technology, USA)

Publisher's Version

Program Verification

A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Clement Blaudeau and Natarajan Shankar
(École Polytechnique, France; SRI International, USA)

Publisher's Version

Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)

Publisher's Version

FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
Thomas Letan and Yann Régis-Gianas
(ANSSI, France; University of Paris, France; IRIF, France; Inria, France)

Publisher's Version

Automated Verification and SAT Solving

Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)

Publisher's Version

Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Johannes Altmanninger and Adrián Rebola Pardo
(TU Vienna, Austria)

Publisher's Version

Proof Engineering and User Interaction

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea)

Publisher's Version

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban
(University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland)

Publisher's Version

REPLica: REPL Instrumentation for Coq Analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner
(University of Washington, USA; University of California at San Diego, USA)

Publisher's Version

Decidability and Complexity

Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)

Publisher's Version

A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Linh Tran, Anshuman Mohan, and Aquinas Hobor
(Yale University, USA; National University of Singapore, Singapore)

Publisher's Version

Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)

Publisher's Version

Homotopy Type Theory

Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)

Publisher's Version

Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani
(University of Strathclyde, UK; LMU Munich, Germany)

Publisher's Version

Mechanized Metatheory

Coq à la Carte: A Practical Approach to Modular Syntax with Binders
Yannick Forster and Kathrin Stark
(Saarland University, Germany)

Publisher's Version

A Mechanized Formalization of GraphQL
Tomás Díaz, Federico Olmedo, and Éric Tanter
(IMFD, Chile; University of Chile, Chile; Inria, France)

Publisher's Version

ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)

Publisher's Version Info

Verified Cryptography

Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL
David Butler, David Aspinall, and Adrià Gascón
(Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK)

Publisher's Version

Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, Estonia)

Publisher's Version

Concurrency and Linearity

Formalizing Determinacy of Concurrent Revisions
Roy Overbeek
(Vrije Universiteit Amsterdam, Netherlands)

Publisher's Version

Formalizing 𝜋-Calculus in Guarded Cubical Agda
Niccolò Veltri and Andrea Vezzosi
(Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark)

Publisher's Version

Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)

Publisher's Version

Formalized Mathematics 1

Formalising Perfectoid Spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot
(Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France)

Publisher's Version Info

A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Kr Singh and Raja Natarajan
(Tata Institute of Fundamental Research, India)

Publisher's Version

Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Christian Doczkal and Damien Pous
(University of Côte d'Azur, France; Inria, France; University of Lyon, France; CNRS, France; ENS Lyon, France)

Publisher's Version Info

Formalized Mathematics 2

The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)

Publisher's Version

A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han and Floris van Doorn
(University of Pittsburgh, USA)

Publisher's Version Info

The Lean Mathematical Library
The mathlib Community

Publisher's Version

proc time: 4.06