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

9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), January 20–21, 2020, New Orleans, LA, USA

CPP 2020 – Proceedings

Contents - Abstracts - Authors

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


Title Page
Welcome from the Chairs

Invited Talks

Matching Logic: The Foundation of the K Framework (Invited Talk)
Grigore Roşu ORCID logo and Xiaohong ChenORCID logo
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
Publisher's Version
Proof Assistants at the Hardware-Software Interface (Invited Talk)
Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version

Program Verification

A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Clement Blaudeau ORCID logo and Natarajan Shankar
(École Polytechnique, France; SRI International, USA)
Publisher's Version
Proof Pearl: Braun Trees
Tobias NipkowORCID logo 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 ORCID logo, and Steve ZdancewicORCID logo
(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 ORCID logo, 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 LernerORCID logo
(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örtbergORCID logo and Loïc Pujet ORCID logo
(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 ORCID logo, and Éric TanterORCID logo
(IMFD, Chile; University of Chile, Chile; Inria, France)
Publisher's Version
ConCert: A Smart Contract Certification Framework in Coq
Danil AnnenkovORCID logo, Jakob Botsch Nielsen, and Bas Spitters ORCID logo
(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 ORCID logo, Casper Bach Poulsen ORCID logo, Robbert KrebbersORCID logo, and Eelco Visser ORCID logo
(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 ORCID logo 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 PousORCID logo
(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: 6.08