POPL 2023 (series) / CPP 2023 (series) /
CPP 2023 Program
This is the CPP 2023 program - see the full program for POPL 2023 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | CompCert: a journey through the landscape of mechanized semantics for verified compilation CPP | ||
10:08 22mTalk | Mechanised Semantics for Gated Static Single Assignment CPP Yann Herklotz Imperial College London, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA DOI Pre-print |
14:00 - 15:30 | |||
14:00 22mTalk | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL CPP Katherine Kosaian Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology | ||
14:22 22mTalk | P4Cub: A Little Language for Big Routers CPP Rudy Peterson Cornell University, Eric Campbell Cornell University, John Chen Cornell University, Natalie Isak Microsoft, Calvin Shyu Cornell University, Ryan Doenges Cornell University, Parsia Ataei Cornell University, Nate Foster Cornell University | ||
14:45 22mTalk | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER CPP Haobin Ni Cornell University, Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research | ||
15:07 22mTalk | Verifying term graph optimizations using Isabelle/HOL CPP Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland, Mark Utting The University of Queensland |
16:00 - 18:00 | Formalized Mathematics ICPP at Studio 1 Chair(s): Adam Chlipala Massachusetts Institute of Technology | ||
16:00 22mTalk | Formalising the h-principle and sphere eversionremote presentation CPP | ||
16:22 22mTalk | A Formalized Reduction of Keller's Conjecture CPP Joshua Clune Carnegie Mellon University | ||
16:45 22mTalk | Computing Cohomology Rings in Cubical Agdadistinguished paper CPP Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay, Axel Ljungström Stockholm University, Anders Mörtberg Department of Mathematics, Stockholm University | ||
17:07 8mBreak | short break CPP | ||
17:15 45mMeeting | CPP Business Meeting CPP Pre-print |
Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 17 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | (canceled invited talk) CPP | ||
10:08 22mTalk | Aesop: White-Box Best-First Proof Search for Leandistinguished paper CPP Link to publication DOI Pre-print |
11:00 - 12:30 | |||
11:00 22mTalk | Terms for Efficient Proof Checking and ParsingRecorded Presentation CPP Michael Färber Universität Innsbruck, Austria | ||
11:22 22mTalk | Compositional pre-processing for automated reasoning in dependent type theoryremote presentation CPP Valentin Blot LMF, Inria, Université Paris-Saclay, Denis Cousineau Mitsubishi Electric R&D Centre Europe, Enzo Crance Mitsubishi Electric R&D Centre Europe, Louise Dubois de Prisque LMF, Inria, Université Paris-Saclay, Chantal Keller LRI, Université Paris-Sud, Assia Mahboubi INRIA, Pierre Vial Inria | ||
11:45 22mTalk | Practical and sound equality tests, automatically CPP | ||
12:07 22mTalk | Compiling higher-order specifications to SMT solvers: how to deal with rejection constructivelyremote presentation CPP Matthew L. Daggitt Heriott-Watt University, Robert Atkey University of Strathclyde, Wen Kokke University of Strathclyde, Ekaterina Komandantskaya Heriot-Watt University, UK, Luca Arnaboldi The University of Edinburgh |
14:00 - 15:30 | |||
14:00 22mTalk | FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Storesremote presentation CPP Arvind Arasu Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Aymeric Fromherz Inria, Kesha Hietala University of Maryland, Bryan Parno Carnegie Mellon University, Ravi Ramamurthy Microsoft Research | ||
14:22 22mTalk | Formalising Decentralised Exchanges in Coq CPP Eske Hoy Nielsen Aarhus University, Danil Annenkov Concordium, Bas Spitters Concordium Blockchain Research Center, Aarhus University | ||
14:45 22mTalk | Semantics of Probabilistic Programs using S-Finite Kernels in Coq CPP Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Cyril Cohen Inria, Ayumu Saito Tokyo Institute of Technology | ||
15:07 22mTalk | Formalising Sharkovsky's Theorem (Proof Pearl) CPP Bhavik Mehta University of Cambridge |
16:00 - 17:30 | |||
16:00 22mTalk | A formalization of Doob's martingale convergence theorems in mathlibremote presentation CPP Kexing Ying University of Cambridge, Rémy Degenne Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9198-CRIStAL, F-59000 Lille, France | ||
16:22 22mTalk | A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL CPP Angeliki Koutsoukou-Argyraki University of Cambridge, Department of Computer Science and Technology, Mantas Bakšys University of Cambridge, Chelsea Edmonds University of Cambridge | ||
16:45 22mTalk | A Formal Disproof of Hirsch Conjecture CPP Xavier Allamigeon Inria and Ecole Polytechnique, Quentin Canu Inria and Ecole Polytechnique, Pierre-Yves Strub Meta | ||
17:07 22mTalk | Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves CPP Anne Baanen Vrije Universiteit Amsterdam, Alex Best Vrije Universiteit Amsterdam, Nirvana Coppola Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam |