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)

Frontmatter

Title Page
Welcome from the Chairs

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 Article Search
Proof Assistants at the Hardware-Software Interface (Invited Talk)
Adam Chlipala
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search

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 Article Search
Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)
Publisher's Version Article Search
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 Article Search

Automated Verification and SAT Solving

Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)
Publisher's Version Article Search
Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Johannes Altmanninger and Adrián Rebola Pardo
(TU Vienna, Austria)
Publisher's Version Article Search

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 Article Search
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 Article Search
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 Article Search

Decidability and Complexity

Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
Publisher's Version Article Search
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 Article Search
Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)
Publisher's Version Article Search

Homotopy Type Theory

Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)
Publisher's Version Article Search
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 Article Search Artifacts Available

Mechanized Metatheory

Coq à la Carte: A Practical Approach to Modular Syntax with Binders
Yannick Forster and Kathrin Stark
(Saarland University, Germany)
Publisher's Version Article Search
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 Article Search
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
Publisher's Version Article Search Info Artifacts Available

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 Article Search
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 Article Search

Concurrency and Linearity

Formalizing Determinacy of Concurrent Revisions
Roy Overbeek
(Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version Article Search
Formalizing 𝜋-Calculus in Guarded Cubical Agda
Niccolò Veltri and Andrea Vezzosi
(Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark)
Publisher's Version Article Search
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 Article Search

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 Article Search 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 Article Search
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 Article Search Info Artifacts Available

Formalized Mathematics 2

The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)
Publisher's Version Article Search
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han and Floris van Doorn
(University of Pittsburgh, USA)
Publisher's Version Article Search Info
The Lean Mathematical Library
The mathlib Community
Publisher's Version Article Search

proc time: 4.01