POPL 2022 (series) / CPP 2022 (series) /
CPP 2022 Program
This is the CPP 2022 program - see the full program for POPL 2022 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:50 - 09:00 | Welcome from the chairsCPP at Salon III Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania | ||
08:50 10mTalk | Chairs' report CPP File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Coq’s vibrant ecosystem for verification engineeringInPerson CPP Link to publication | ||
10:20 - 12:00 | |||
10:20 25mTalk | Specification and Verification of a Transient StackDistinguished Paper AwardRemote CPP DOI Pre-print Media Attached File Attached | ||
10:45 25mTalk | Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly LibraryRemote CPP Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University, Daniel Frumin University of Groningen Pre-print Media Attached | ||
11:10 25mTalk | Applying Formal Verification to Microkernel IPC at MetaInPerson CPP Quentin Carbonneaux Meta, Noam Zilberstein Cornell University, Christoph Klee Facebook, Peter W. O'Hearn Meta; University College London, Francesco Zappa Nardelli Meta Pre-print | ||
11:35 25mTalk | Certified Abstract Machines for Skeletal SemanticsRemote CPP Pre-print Media Attached | ||
15:30 - 17:10 | Security and Distributed SystemsCPP at Salon III Chair(s): Alwyn Goodloe NASA Langley Research Center | ||
15:30 25mTalk | Reflection, Rewinding, and Coin-Toss in EasyCryptRemote CPP Pre-print Media Attached | ||
15:55 25mTalk | A verified algebraic representation of Cairo program executionRemote CPP Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd. Pre-print | ||
16:20 25mTalk | Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson CPP William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University Pre-print | ||
16:45 25mTalk | Forward build systems, formallyInPerson CPP Link to publication | ||
17:30 - 18:30 | |||
17:30 60mTalk | The seL4 verification: the art and craft of proof and the reality of commercial supportRemote CPP Media Attached | ||
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mTalk | Structural Embeddings RevisitedRemote CPP | ||
10:20 - 12:00 | Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III Chair(s): Steve Zdancewic University of Pennsylvania | ||
10:20 25mTalk | CertiStr: A Certified String SolverDistinguished Paper AwardRemote CPP Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern DOI Pre-print Media Attached | ||
10:45 25mTalk | Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote CPP Michael Färber Universität Innsbruck, Austria DOI Pre-print Media Attached File Attached | ||
11:10 25mTalk | An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote CPP Pre-print Media Attached | ||
11:35 25mTalk | A Drag-and-Drop Proof TacticRemote CPP Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique DOI Pre-print Media Attached | ||
13:30 - 15:10 | Formalization of Logic, Algebra and GeometryCPP at Salon III Chair(s): Andrei Popescu University of Sheffield | ||
13:30 25mTalk | Semantic cut elimination for the logic of bunched implications, formalized in CoqDistinguished Paper AwardRemote CPP Daniel Frumin University of Groningen Pre-print Media Attached | ||
13:55 25mTalk | Undecidability, Incompleteness, and Completeness of Second-Order Logic in CoqRemote CPP Pre-print | ||
14:20 25mTalk | Formalising Lie algebrasRemote CPP Oliver Nash Imperial College, London Pre-print Media Attached | ||
14:45 25mTalk | A Machine-Checked Direct Proof of the Steiner-Lehmus TheoremInPerson CPP Ariel E. Kellison Cornell University Pre-print | ||
15:30 - 16:10 | Chairs' Report and Business MeetingCPP at Salon III Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania | ||
15:30 40mTalk | Chairs' Report CPP File Attached | ||
16:30 - 18:10 | Category Theory, HoTT, Number TheoryCPP at Salon III Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota | ||
16:30 25mTalk | Implementing a category-theoretic framework for typed abstract syntaxRemote CPP Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University DOI Pre-print Media Attached | ||
16:55 25mTalk | (Deep) Induction Rules for GADTsRemote CPP Pre-print Media Attached | ||
17:20 25mTalk | On homotopy of walks and spherical maps in homotopy type theoryRemote CPP Jonathan Prieto-Cubides University of Bergen Pre-print Media Attached | ||
17:45 25mTalk | Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote CPP Hing Lun Chan Australian National University DOI Pre-print Media Attached File Attached | ||