POPL 2020 (series) / CPP 2020 (series) /
CPP 2020 Program
This is the CPP 2020 program - see the full program for POPL 2020 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 20 JanDisplayed time zone: Saskatchewan, Central America change
Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change
09:00 - 10:00 | |||
09:00 60mTalk | Invited talk: Matching Logic: The Foundation of the K Framework CPP Grigore Roşu University of Illinois at Urbana-Champaign, Xiaohong Chen University of Illinois at Urbana-Champaign DOI Media Attached |
10:30 - 11:35 | |||
10:30 21mTalk | A Verified Packrat Parser Interpreter for Parsing Expression Grammars CPP DOI Pre-print Media Attached | ||
10:51 22mTalk | Proof Pearl: Braun Trees CPP Tobias Nipkow Technische Universität München, Thomas Sewell Chalmers University of Technology, Sweden DOI Pre-print Media Attached | ||
11:13 22mTalk | FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq CPP DOI Pre-print Media Attached |
11:45 - 12:30 | |||
11:45 22mTalk | Verifying x86 Instruction Implementations CPP Shilpi Goel Centaur Technology, Inc., Anna Slobodova Centaur Technology, Inc., Rob Sumners Centaur Technology, Inc., Sol Swords Centaur Technology, Inc. DOI Pre-print File Attached | ||
12:07 22mTalk | Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs CPP DOI Pre-print Media Attached |
14:00 - 15:05 | |||
14:00 21mTalk | An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction CPP Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University of Pennsylvania DOI Pre-print Media Attached File Attached | ||
14:21 21mTalk | Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar CPP Qingxiang Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in Prague DOI Pre-print | ||
14:43 21mTalk | REPLICA: REPL Instrumentation for Coq Analysis CPP Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University of California, San Diego DOI Pre-print Media Attached |
15:35 - 16:40 | |||
15:35 21mTalk | Verified Programming of Turing Machines in Coq CPP Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland University DOI Pre-print Media Attached | ||
15:56 21mTalk | A Functional Proof Pearl: Inverting the Ackermann Hierarchy CPP Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore DOI Pre-print Media Attached | ||
16:18 21mTalk | Undecidability of Higher-Order Unification Formalised in Coq CPP DOI Pre-print Media Attached |
16:50 - 17:56 | Homotopy Type Theory and PC chairs' reportCPP at Maurepas Chair(s): Floris van Doorn University of Pittsburgh | ||
16:50 22mTalk | Cubical Synthetic Homotopy Theory CPP Anders Mörtberg Department of Mathematics, Stockholm University, Loïc Pujet Gallinette Project-Team, Inria DOI Pre-print Media Attached File Attached | ||
17:12 22mTalk | Three equivalent ordinal notation systems in Cubical Agda CPP Fredrik Nordvall Forsberg University of Strathclyde, Chuangjie Xu Ludwig-Maximilians-Universität München, Neil Ghani University of Strathclyde DOI Pre-print Media Attached File Attached | ||
17:34 22mTalk | PC Chairs' report CPP DOI Media Attached File Attached |
Tue 21 JanDisplayed time zone: Saskatchewan, Central America change
Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change
09:00 - 10:00 | |||
09:00 60mTalk | Invited talk: Proof Assistants at the Hardware-Software Interface CPP Adam Chlipala Massachusetts Institute of Technology DOI Media Attached |
10:30 - 11:35 | |||
10:30 21mTalk | Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP DOI Pre-print Media Attached | ||
10:51 21mTalk | A Mechanized Formalization of GraphQL CPP Tomás Díaz IMFD Chile, Federico Olmedo University of Chile & IMFD Chile, Éric Tanter University of Chile DOI Pre-print Media Attached File Attached | ||
11:13 21mTalk | ConCert: A Smart Contract Certification Framework in Coq CPP Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached |
11:45 - 12:30 | |||
11:45 22mTalk | Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL CPP David Butler Alan Turing Institute, David Aspinall University of Edinburgh, Adria Gascon Alan Turing Institute DOI Pre-print Media Attached | ||
12:07 22mTalk | Verified Security of BLT Signature Scheme CPP Denis Firsov Guardtime AS, Ahto Buldas Tallinn University of Technology, Ahto Truu Guardtime AS, Risto Laanoja Guardtime AS DOI Pre-print Media Attached File Attached |
14:00 - 15:05 | |||
14:00 21mTalk | Formalizing Determinacy of Concurrent Revisions CPP Roy Overbeek Vrije Universiteit Amsterdam DOI Pre-print Media Attached | ||
14:21 21mTalk | Formalizing π-calculus in Guarded Cubical Agda CPP DOI Pre-print Media Attached File Attached | ||
14:43 21mTalk | Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages CPP Arjen Rouvoet Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology DOI Pre-print Media Attached File Attached |
15:35 - 16:40 | |||
15:35 21mTalk | Formalising perfectoid spaces CPP Patrick Massot Université Paris Sud, Kevin Buzzard Imperial College London, Johan Commelin Universität Freiburg DOI Pre-print Media Attached File Attached | ||
15:56 21mTalk | A Constructive Formalization of the Weak Perfect Graph Theorem CPP Abhishek Kr Singh Tata Institute of Fundamental Research Mumbai, Raja Natarajan Tata Institute of Fundamental Research Mumbai DOI Pre-print Media Attached File Attached | ||
16:18 21mTalk | Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq CPP DOI Pre-print Media Attached |
16:50 - 17:56 | |||
16:50 22mTalk | The Poincaré-Bendixson Theorem in Isabelle/HOL CPP DOI Pre-print Media Attached | ||
17:12 22mTalk | A Formal Proof of the Independence of the Continuum Hypothesis CPP DOI Pre-print Media Attached | ||
17:34 22mTalk | The Lean mathematical library CPP DOI Pre-print Media Attached File Attached |