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
Article: poplws20cppforeword-fm000-p doi:
Welcome from the Chairs
Article: poplws20cppforeword-fm001-p doi:

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: poplws20cppmain-k2-p doi:10.1145/3372885.3378574
Proof Assistants at the Hardware-Software Interface (Invited Talk)
Adam Chlipala
(Massachusetts Institute of Technology, USA)
Publisher's Version Article: poplws20cppmain-k1-p doi:10.1145/3372885.3378575

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: poplws20cppmain-p77-p doi:10.1145/3372885.3373836
Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)
Publisher's Version Article: poplws20cppmain-p73-p doi:10.1145/3372885.3373834
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: poplws20cppmain-p42-p doi:10.1145/3372885.3373812

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: poplws20cppmain-p38-p doi:10.1145/3372885.3373811
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: poplws20cppmain-p21-p doi:10.1145/3372885.3373821

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: poplws20cppmain-p44-p doi:10.1145/3372885.3373813
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: poplws20cppmain-p47-p doi:10.1145/3372885.3373827
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: poplws20cppmain-p27-p doi:10.1145/3372885.3373823

Decidability and Complexity

Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
Publisher's Version Article: poplws20cppmain-p63-p doi:10.1145/3372885.3373816
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: poplws20cppmain-p87-p doi:10.1145/3372885.3373837
Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)
Publisher's Version Article: poplws20cppmain-p62-p doi:10.1145/3372885.3373832

Homotopy Type Theory

Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)
Publisher's Version Article: poplws20cppmain-p30-p doi:10.1145/3372885.3373825
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 Published Artifact Artifacts Available Article: poplws20cppmain-p74-p doi:10.1145/3372885.3373835

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: poplws20cppmain-p64-p doi:10.1145/3372885.3373817
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: poplws20cppmain-p22-p doi:10.1145/3372885.3373822
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Article: poplws20cppmain-p50-p doi:10.1145/3372885.3373829

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: poplws20cppmain-p48-p doi:10.1145/3372885.3373815
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: poplws20cppmain-p49-p doi:10.1145/3372885.3373828

Concurrency and Linearity

Formalizing Determinacy of Concurrent Revisions
Roy Overbeek
(Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version Article: poplws20cppmain-p19-p doi:10.1145/3372885.3373820
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: poplws20cppmain-p46-p doi:10.1145/3372885.3373814
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 Published Artifact Artifacts Available Article: poplws20cppmain-p83-p doi:10.1145/3372885.3373818

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: poplws20cppmain-p59-p doi:10.1145/3372885.3373830
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: poplws20cppmain-p9-p doi:10.1145/3372885.3373819
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 Published Artifact Artifacts Available Article: poplws20cppmain-p60-p doi:10.1145/3372885.3373831

Formalized Mathematics 2

The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)
Publisher's Version Article: poplws20cppmain-p68-p doi:10.1145/3372885.3373833
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: poplws20cppmain-p36-p doi:10.1145/3372885.3373826
The Lean Mathematical Library
The mathlib Community
Publisher's Version Article: poplws20cppmain-p29-p doi:10.1145/3372885.3373824

proc time: 0.07