POPL 2023
Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States
POPL 2023 (series) / Boston Park Plaza /

Room information: Studio 1

VenueBoston Park Plaza
Room nameStudio 1
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
CompCert and BeyondCPP at Studio 1
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Keynote
CompCert: a journey through the landscape of mechanized semantics for verified compilation
CPP
K: Sandrine Blazy University of Rennes; Inria; CNRS; IRISA
10:08
22m
Talk
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
11:00 - 12:30
Logical FoundationsCPP at Studio 1
Chair(s): Robbert Krebbers Radboud University Nijmegen
11:00
22m
Talk
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systemsdistinguished paper
CPP
Christina Kohl University of Innsbruck, Aart Middeldorp University of Innsbruck
11:22
22m
Talk
Formalizing and computing propositional quantifiersremote presentation
CPP
Hugo Férée Université Paris Cité / IRIF, Sam van Gool Université Paris Cité / IRIF
11:45
22m
Talk
Encoding Dependently-Typed Constructions into Simple Type Theoryremote presentation
CPP
Anthony Bordg University of Cambridge, Adrián Doña Mateo The University of Edinburgh
12:07
22m
Talk
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
CPP
Yannick Forster Inria, Felix Jahn Saarland University, Gert Smolka Saarland University
14:00 - 15:30
Languages and CompilersCPP at Studio 1
Chair(s): Cody Roux AWS
14:00
22m
Talk
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
22m
Talk
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
22m
Talk
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
22m
Talk
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
22m
Talk
Formalising the h-principle and sphere eversionremote presentation
CPP
Patrick Massot , Floris van Doorn University of Pittsburgh, Oliver Nash Imperial College, London
16:22
22m
Talk
A Formalized Reduction of Keller's Conjecture
CPP
Joshua Clune Carnegie Mellon University
16:45
22m
Talk
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
8m
Break
short break
CPP

17:15
45m
Meeting
CPP Business Meeting
CPP

Pre-print

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Proof SearchCPP at Studio 1
Chair(s): Brigitte Pientka McGill University
09:00
60m
Keynote
(canceled invited talk)
CPP

10:08
22m
Talk
Aesop: White-Box Best-First Proof Search for Leandistinguished paper
CPP
Jannis Limperg Vrije Universiteit Amsterdam, Asta Halkjær From Technical University of Denmark
Link to publication DOI Pre-print
11:00 - 12:30
Practical ProvingCPP at Studio 1
Chair(s): Dmitriy Traytel University of Copenhagen
11:00
22m
Talk
Terms for Efficient Proof Checking and ParsingRecorded Presentation
CPP
Michael Färber Universität Innsbruck, Austria
11:22
22m
Talk
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
22m
Talk
Practical and sound equality tests, automatically
CPP
Benjamin Gregoire INRIA, Jean-Christophe Léchenet Université Côte d’Azur, Inria, Enrico Tassi INRIA
12:07
22m
Talk
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
ApplicationsCPP at Studio 1
Chair(s): Yoonseung Kim Yale University
14:00
22m
Talk
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
22m
Talk
Formalising Decentralised Exchanges in Coq
CPP
Eske Hoy Nielsen Aarhus University, Danil Annenkov Concordium, Bas Spitters Concordium Blockchain Research Center, Aarhus University
14:45
22m
Talk
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
22m
Talk
Formalising Sharkovsky's Theorem (Proof Pearl)
CPP
Bhavik Mehta University of Cambridge
16:00 - 17:30
Formalized Mathematics IICPP at Studio 1
Chair(s): Viktor Vafeiadis MPI-SWS
16:00
22m
Talk
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
22m
Talk
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
22m
Talk
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
22m
Talk
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

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Studio 1

CPP

CompCert and Beyond

CPP

Logical Foundations

CPP

Languages and Compilers

CPP

Formalized Mathematics I

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Studio 1

CPP

Proof Search

CPP

Practical Proving

CPP

Applications

CPP

Formalized Mathematics II

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Studio 1
CPP
CompCert: a journey through the landscape of mechanized semantics for v ...
09:00 - 10:00
CPP
Mechanised Semantics for Gated Static Single Assignment
10:08 - 10:30
CPPdistinguished paper
A Formalization of the Development Closedness Criterion for Left-Linear ...
11:00 - 11:22
CPPremote presentation
Formalizing and computing propositional quantifiers
11:22 - 11:45
CPPremote presentation
Encoding Dependently-Typed Constructions into Simple Type Theory
11:45 - 12:07
CPP
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Co ...
12:07 - 12:30
CPP
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
14:00 - 14:22
CPP
P4Cub: A Little Language for Big Routers
14:22 - 14:45
CPP
ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
14:45 - 15:07
CPP
Verifying term graph optimizations using Isabelle/HOL
15:07 - 15:30
CPPremote presentation
Formalising the h-principle and sphere eversion
16:00 - 16:22
CPP
A Formalized Reduction of Keller's Conjecture
16:22 - 16:44
CPPdistinguished paper
Computing Cohomology Rings in Cubical Agda
16:45 - 17:07
CPP
short break
17:07 - 17:15
CPP
CPP Business Meeting
17:15 - 18:00

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Studio 1
CPP
(canceled invited talk)
09:00 - 10:00
CPPdistinguished paper
Aesop: White-Box Best-First Proof Search for Lean
10:08 - 10:30
CPPRecorded Presentation
Terms for Efficient Proof Checking and Parsing
11:00 - 11:22
CPPremote presentation
Compositional pre-processing for automated reasoning in dependent type ...
11:22 - 11:45
CPP
Practical and sound equality tests, automatically
11:45 - 12:07
CPPremote presentation
Compiling higher-order specifications to SMT solvers: how to deal with ...
12:07 - 12:30
CPPremote presentation
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
14:00 - 14:22
CPP
Formalising Decentralised Exchanges in Coq
14:22 - 14:45
CPP
Semantics of Probabilistic Programs using S-Finite Kernels in Coq
14:45 - 15:07
CPP
Formalising Sharkovsky's Theorem (Proof Pearl)
15:07 - 15:30
CPPremote presentation
A formalization of Doob's martingale convergence theorems in mathlib
16:00 - 16:22
CPP
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
16:22 - 16:45
CPP
A Formal Disproof of Hirsch Conjecture
16:45 - 17:07
CPP
Formalized Class Group Computations and Integral Points on Mordell Elli ...
17:07 - 17:30