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

POPL 2020 Co-Located Events, January 19–25, 2020, New Orleans, LA, USA

POPL 2020 Co-Located Events – Preliminary Table of Contents

Contents - Abstracts - Authors

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


Title Page
Welcome from the Chairs
CPP 2020 Organization


Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, n.n.)
Article Search
Astructio: Specifying, Verifying, and Executing Impure Computations in Coq
Thomas Letan and Yann Régis-Gianas
(ANSSI, France; IRIF, France; Inria, France)
Article Search
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)
Article Search
Formalizing 𝜋-Calculus in Guarded Cubical Agda
Niccolò Veltri and Andrea Vezzosi
(Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark)
Article Search
Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL
David Butler, David Aspinall, and Adria Gascon
(Alan Turing Institute, UK; University of Edinburgh, UK)
Article Search
Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
Article Search
Coq à la Carte: A Practical Approach to Modular Syntax with Binders
Yannick Forster and Kathrin Stark
(Saarland University, Germany)
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)
Article Search
A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Kr Singh and Raja Natarajan
(Tata Institute of Fundamental Research Mumbai, India)
Article Search
Formalizing Determinacy of Concurrent Revisions
Roy Overbeek
(CWI, Netherlands)
Article Search
Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Adrian Rebola Pardo and Johannes Altmanninger
(TU Vienna, Austria)
Article Search
A Mechanized Formalization of GraphQL
Tomás Díaz, Federico Olmedo, and Éric Tanter
(IMFD, Chile; University of Chile, Chile; Inria, France)
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)
Article Search
The Lean Mathematical Library
The mathlib Community
Article Search
Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)
Article Search
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han and Floris van Doorn
(University of Pittsburgh, USA)
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)
Article Search
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, n.n.)
Article Search
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
Article Search
Formalising Perfectoid Spaces
Patrick Massot, Kevin Buzzard, and Johan Commelin
(University of Paris-Sud, France; Imperial College London, UK; University of Freiburg, Germany)
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; CNRS, France; ENS Lyon, France)
Article Search
Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)
Article Search
The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)
Article Search
Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)
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)
Article Search
A Verified Packrat Parser Generator for Parsing Expression Grammars
Clement Blaudeau and Natarajan Shankar
(Ecole Polytechnique, n.n.; SRI International Computer Science Laboratory, n.n.)
Article Search
Inverting the Ackermann Hierarchy
Linh Tran, Anshuman Mohan, and Aquinas Hobor
(National University of Singapore, Singapore)
Article Search

2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2020)


Title Page
Message from the Chairs

Research Papers

Module Generation without Regret
Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe
(University of Tsukuba, Japan)
Article Search
Symbolic Bisimulation for Open and Parameterized Systems
Zechen Hou and Eric Madelaine
(East China Normal University, China; Inria, France)
Article Search
High-Fidelity Metaprogramming with Separator Syntax Trees
Rodin T. A. Aarssen and Tijs van der Storm
(CWI, Netherlands; Eindhoven University of Technology, Netherlands; University of Groningen, Netherlands)
Article Search

Short Papers

An Approach to Generate Text-Based IDEs for Syntax Completion Based on Syntax Specification
Isao Sasano
(Shibaura Institute of Technology, Japan)
Article Search
GOOL: A Generic Object-Oriented Language
Jacques Carette, Brooks MacLachlan, and Spencer Smith
(McMaster University, Canada)

proc time: 5.91