Salon III - POPL 2022

VenueWestin Philadelphia

Room nameSalon III

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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

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

09:00 - 09:45	Research keynoteProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

09:00 45m Keynote		Research keynote -- Programming Languages and Law: A Research Agenda for a New FieldRemote ProLaLa James Grimmelmann Cornell University File Attached

09:45 - 10:05	Long talks #1ProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

09:45 20m Talk		Legal CalculiInPerson ProLaLa Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University File Attached

10:20 - 12:00	Long talks #2ProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

10:20 20m Talk		Position Paper: LLD is All You NeedRemote ProLaLa L. Thorne McCarty Rutgers, The State University of New Jersey Pre-print
10:40 20m Talk		Logical English as a Programming Language for the LawRemote ProLaLa Robert Kowalski Imperial College London, Jacinto Dávila Contratos Lógicos. C.A. and Universidad de Los Andes, Miguel Calejo logicalcontracts.com File Attached
11:00 20m Talk		Introduction of PROLEG (PROlog-based LEGal reasoning support system)Remote ProLaLa Ken Satoh National Institute of Informatics, Wachara Fungwacharakorn National Institute of Informatics, Kanae Tsushima National Institute of Informatics, Japan File Attached
11:20 20m Talk		DPCL: a Language Template for Normative SpecificationsRemote ProLaLa Giovanni Sileno University of Amsterdam, Thomas van Binsbergen University of Amsterdam, Matteo Pascucci Slovak Academy of Science, Tom van Engers Leibniz Institute / University of Amsterdam / TNO Pre-print
11:40 20m Talk		Reflections on the design and application of eFLINTRemote ProLaLa L. Thomas van Binsbergen CWI Pre-print File Attached

13:30 - 14:10	Short talksProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

13:30 10m Talk		Littleton: An Educational Environment for Property LawRemote ProLaLa Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University File Attached
13:40 10m Talk		Modeling Administrative Discretion Using Goal-Directed Answer Set ProgrammingRemote ProLaLa Joaquín Arias Universidad Rey Juan Carlos, Mar Moreno-Rebato Universidad Rey Juan Carlos, José Antonio Rodríguez-García Universidad Rey Juan Carlos, Sascha Ossowski Universidad Rey Juan Carlos Pre-print Media Attached File Attached
13:50 10m Talk		Probabilistic programming for Employment Tribunal remediesRemote ProLaLa James Cheney University of Edinburgh; Alan Turing Institute
14:00 10m Talk		Prevalence of Expression Types in Legislative TextRemote ProLaLa Jason Morris Service Canada, Lexpedite Legal Technology

14:10 - 14:50	Long talks #3ProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

14:10 20m Talk		Law Smells: Defining and Detecting Problematic Patterns in Legal DraftingRemote ProLaLa Corinna Coupette Max Planck Institute for Informatics, Saarbrücken, Germany, Dirk Hartung Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany, Janis Beckedorf Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany, Maximilian Böther Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Daniel Martin Katz Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA Pre-print File Attached
14:30 20m Talk		Cod(e)ifying The LawInPerson ProLaLa Nel Escher University of Michigan, Jeffrey Bilik University of Michigan, Alexander Miller University of Michigan, Jennifer Jiyoung Huseby University of Michigan, Divya Ramesh University of Michigan, Alice Liu University of Michigan, Sam Mikell University of Michigan, Nina Cahill University of Michigan, Ben Green University of Michigan, Nikola Banovic University of Michigan File Attached

15:05 - 15:25	Long talks #4ProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

15:05 20m Talk		Stipula: a domain specific language for legal contractsRemote ProLaLa Silvia Crafa University of Padova, Cosimo Laneve University of Bologna, Giovanni Sartor University of Bologna Pre-print File Attached

15:25 - 16:10	Industry keynoteProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

15:25 45m Industry talk		Industry keynote -- What does a toolchain for legislation eventually become?Remote ProLaLa Davin Fifield Oracle, Surend Dayal Australian National University, Don Syme Microsoft Link to publication

16:10 - 16:30	Long talks #5ProLaLa at Salon III Chair(s): Jonathan Protzenko Microsoft Research, Redmond

16:10 20m Talk		Ergo - a programming language for Smart Legal ContractsRemote ProLaLa Niall Roche Mishcon de Reya,University College London,Accord Project, Jerome Simeon Clause, Walter Hernandez Mishcon de Reya,Accord Project, Eason Chen Accord Project, Dan Selman Docusign,Accord Project Pre-print File Attached

16:40 - 17:40	Long talks #6ProLaLa at Salon III Chair(s): Shrutarshi Basu Harvard University

16:40 20m Talk		A General Library of Legal ComponentsRemote ProLaLa Chris Bailey University of Illinois College of Law Link to publication
17:00 20m Talk		Overview of the CCLAW L4 projectRemote ProLaLa Avishkar Mahajan Singapore Management University, Martin Strecker Singapore Management University, Meng Weng Wong Singapore Management University
17:20 20m Talk		Turning Catala into a Proof Platform for the LawRemote ProLaLa Alain Delaët INRIA, ENS Lyon, Denis Merigoux INRIA, Aymeric Fromherz Inria Pre-print

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 10m Talk		Chairs' report CPP File Attached

09:00 - 10:00	Invited TalkCPP at Salon III Chair(s): Steve Zdancewic University of Pennsylvania

09:00 60m Talk		Coq’s vibrant ecosystem for verification engineeringInPerson CPP I: Andrew W. Appel Princeton Link to publication

10:20 - 12:00	Verified Data Structures and SemanticsCPP at Salon III Chair(s): Jeehoon Kang KAIST

10:20 25m Talk		Specification and Verification of a Transient StackDistinguished Paper AwardRemote CPP Alexandre Moine Inria, Arthur Charguéraud Inria, François Pottier Inria DOI Pre-print Media Attached File Attached
10:45 25m Talk		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 25m Talk		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 25m Talk		Certified Abstract Machines for Skeletal SemanticsRemote CPP Guillaume Ambal Univ. Rennes, Sergueï Lenglet Université de Lorraine, France, Alan Schmitt Inria Pre-print Media Attached

13:30 - 15:10	Semantics and Program VerificationCPP at Salon III Chair(s): Benjamin Delaware Purdue University

13:30 25m Talk		A Compositional Proof Framework for FRETish RequirementsRemote CPP Esther Conrad NASA LaRC, Laura Titolo NIA/NASA LaRC, Dimitra Giannakopoulou NASA Ames Research Center, Thomas Pressburger NASA ARC, Aaron Dutle NASA Langley Research Center Pre-print Media Attached
13:55 25m Talk		Verbatim++: Verified, Optimized, and Semantically Rich Lexing with DerivativesRemote CPP Derek Egolf Northeastern University, Sam Lasser Tufts University, Kathleen Fisher Tufts University Link to publication Media Attached
14:20 25m Talk		Formally Verified Superblock SchedulingInPerson CPP Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Léo Gourdin Université Grenoble-Alpes, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Justus Fasse Université Grenoble-Alpes; KU Leuven, Nicolas Nardino École normale supérieure de Lyon DOI Pre-print
14:45 25m Talk		Overcoming Restraint: Composing Verification of Foreign Functions with CogentRemote CPP Louis Cheung University of Melbourne, Liam O'Connor University of Edinburgh, Christine Rizkallah University of Melbourne DOI 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 25m Talk		Reflection, Rewinding, and Coin-Toss in EasyCryptRemote CPP Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu Pre-print Media Attached
15:55 25m Talk		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 25m Talk		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 25m Talk		Forward build systems, formallyInPerson CPP Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University Link to publication

17:30 - 18:30	Invited TalkCPP at Salon III Chair(s): Andrei Popescu University of Sheffield

17:30 60m Talk		The seL4 verification: the art and craft of proof and the reality of commercial supportRemote CPP I: June Andronick Proofcraft, UNSW and seL4 Foundation Media Attached

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

09:00 - 10:00	Invited TalkCPP at Salon III Chair(s): Laura Titolo NIA/NASA LaRC

09:00 60m Talk		Structural Embeddings RevisitedRemote CPP I: Cesar Munoz AWS

10:20 - 12:00	Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III Chair(s): Steve Zdancewic University of Pennsylvania

10:20 25m Talk		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 25m Talk		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 25m Talk		An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote CPP Mihails Milehins Pre-print Media Attached
11:35 25m Talk		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 25m Talk		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 25m Talk		Undecidability, Incompleteness, and Completeness of Second-Order Logic in CoqRemote CPP Mark Koch Saarland University, Dominik Kirst Saarland University Pre-print
14:20 25m Talk		Formalising Lie algebrasRemote CPP Oliver Nash Imperial College, London Pre-print Media Attached
14:45 25m Talk		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 40m Talk		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 25m Talk		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 25m Talk		(Deep) Induction Rules for GADTsRemote CPP Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology Pre-print Media Attached
17:20 25m Talk		On homotopy of walks and spherical maps in homotopy type theoryRemote CPP Jonathan Prieto-Cubides University of Bergen Pre-print Media Attached
17:45 25m Talk		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

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

10:20 - 12:00	Separation LogicPOPL at Salon III Chair(s): James Riely DePaul University

10:20 25m Talk		A Separation Logic for Heap Space under Garbage CollectionRemote POPL Jean-Marie Madiot Inria, François Pottier Inria DOI Media Attached
10:45 25m Research paper		Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote POPL Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS DOI Media Attached
11:10 25m Research paper		Concurrent Incorrectness Separation LogicRemote POPL Azalea Raad Imperial College London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI Media Attached
11:35 25m Research paper		On Incorrectness Logic and Kleene Algebra with Top and TestsInPerson POPL Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University DOI Media Attached

13:30 - 14:45	Weak Memory ModelsPOPL at Salon III Chair(s): Mae Milano University of California, Berkeley

13:30 25m Research paper		The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson POPL Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University DOI Media Attached
13:55 25m Research paper		Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal StoresRemote POPL Azalea Raad Imperial College London, Luc Maranget Inria, Viktor Vafeiadis MPI-SWS DOI Media Attached
14:20 25m Research paper		Truly Stateless, Optimal Dynamic Partial Order ReductionRemote POPL Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS DOI Media Attached

15:05 - 16:20	Concurrency and ParallelismPOPL at Salon III Chair(s): Andrew Myers Cornell University

15:05 25m Research paper		Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote POPL Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute DOI Media Attached
15:30 25m Research paper		Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote POPL Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen DOI Media Attached
15:55 25m Research paper		Static Prediction of Parallel Computation GraphsInPerson POPL Stefan K. Muller Illinois Institute of Technology DOI Media Attached

16:40 - 17:30	Reasoning about Probabilistic Programs and AlgorithmsPOPL at Salon III Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology

16:40 25m Research paper		A Separation Logic for Negative DependenceRemote POPL Jialu Bao Cornell University, Marco Gaboardi Boston University, Justin Hsu Cornell University, Joseph Tassarotti Boston College DOI Media Attached
17:05 25m Research paper		Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote POPL Yizhou Zhang University of Waterloo, Nada Amin Harvard University DOI Media Attached

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

10:20 - 12:00	Quantum ComputingPOPL at Salon III Chair(s): Michael Hicks University of Maryland at College Park

10:20 25m Research paper		Quantum Information EffectsRemote POPL Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Edinburgh DOI Media Attached
10:45 25m Research paper		Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson POPL Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI Media Attached
11:10 25m Research paper		A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote POPL Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University DOI Media Attached
11:35 25m Research paper		Semantics for Variational Quantum ProgrammingRemote POPL Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria DOI Media Attached

13:30 - 14:45	Dynamic AnalysisPOPL at Salon III Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology

13:30 25m Research paper		A Formal Foundation for Symbolic Evaluation with MergingRemote POPL Sorawee Porncharoenwase University of Washington, Luke Nelson University of Washington, Xi Wang University of Washington, Emina Torlak University of Washington DOI Media Attached
13:55 25m Research paper		Logarithm and Program TestingInPerson POPL Kuen-Bang Hou (Favonia) University of Minnesota, Zhuyang Wang University of Minnesota DOI Media Attached
14:20 25m Research paper		Profile Inference RevisitedRemote POPL Wenlei He Facebook, Julián Mestre Facebook; University of Sydney, Sergey Pupyrev , Lei Wang Facebook, Hongtao Yu Facebook DOI Media Attached

15:05 - 16:20	MetaprogrammingPOPL at Salon III Chair(s): Stephanie Weirich University of Pennsylvania

15:05 25m Research paper		Staging with Class: A Specification for Typed Template HaskellInPerson POPL Ningning Xie University of Toronto, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol DOI Media Attached
15:30 25m Research paper		Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote POPL Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University DOI Media Attached
15:55 25m Research paper		Type-Level Programming with Match TypesRemote POPL Olivier Blanvillain EPFL, Jonathan Immanuel Brachthäuser University of Tübingen, Maxime Kjaer EPFL, Martin Odersky EPFL DOI Media Attached

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

10:20 - 12:00	Semantics 1POPL at Salon III Chair(s): Alan Jeffrey Roblox

10:20 25m Research paper		From Enhanced Coinduction towards Enhanced InductionRemote POPL Davide Sangiorgi University of Bologna; Inria DOI Media Attached
10:45 25m Research paper		A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson POPL Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France DOI Media Attached
11:10 25m Research paper		Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote POPL Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford DOI Media Attached
11:35 25m Research paper		Layered and Object-Based Game SemanticsInPerson POPL Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS; Université de Paris, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS DOI Media Attached

13:30 - 14:45	Semantics 2POPL at Salon III Chair(s): Marco Gaboardi Boston University

13:30 25m Research paper		Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson POPL Vikraman Choudhury Indiana University; University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University Link to publication DOI Media Attached
13:55 25m Research paper		A Relational Theory of Effects and CoeffectsRemote POPL Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria DOI Media Attached
14:20 25m Research paper		Effectful Program DistancingRemote POPL Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria DOI Media Attached

15:05 - 16:20	Type TheoryPOPL at Salon III Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota

15:05 25m Research paper		A Cost-Aware Logical FrameworkInPerson POPL Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI Media Attached
15:30 25m Research paper		Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote POPL Marcelo Fiore University of Cambridge, Dmitrij Szamozvancev University of Cambridge DOI Media Attached
15:55 25m Research paper		Observational Equality: Now for GoodDistinguished PaperRemote POPL Loïc Pujet Inria, Nicolas Tabareau Inria DOI Media Attached

16:40 - 17:30	SynthesisPOPL at Salon III Chair(s): Paul Downen University of Massachusetts Lowell

16:40 25m Research paper		Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson POPL Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI Media Attached
17:05 25m Research paper		Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote POPL Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI Media Attached

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

09:00 - 10:00	Session 1WITS at Salon III Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag

09:00 15m Talk		CN: A Refinement Type System for CRemote WITS Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
09:15 45m Other		Type-aware equational rewriting (discussion)In-Person WITS Richard A. Eisenberg Tweag
09:15 45m Other		Multi case trees: confluence and coverage (discussion)In-Person WITS Tesla Zhang The Pennsylvania State University
09:15 45m Other		Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote WITS Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology File Attached
09:15 45m Other		The Expression Problem and Theorem Proving (discussion)Remote WITS Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania

10:20 - 12:00	Session 2WITS at Salon III Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag

10:20 45m Keynote		Make Three To Throw Away: Frontiers in Homotopical Proof AssistantsRemote WITS Jonathan Sterling Aarhus University
11:05 15m Talk		The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoqRemote WITS Matthieu Sozeau Inria, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Yannick Forster Inria
11:20 40m Other		Elaborator reflection APIs (discussion)Remote WITS Jesper Cockx TU Delft
11:20 40m Other		Invisible arguments: language design (discussion)In-Person WITS Richard A. Eisenberg Tweag

13:30 - 14:45	Session 3WITS at Salon III Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag

13:30 15m Talk		Tries that matchRemote WITS Sebastian Graf Karlsruhe Institute of Technology
13:45 15m Talk		Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote WITS Sebastian Ullrich Karlsruhe Institute of Technology
14:00 45m Other		Benchmarking Binding (discussion)In-Person WITS Stephanie Weirich University of Pennsylvania
14:00 45m Other		Fancy module systems (discussion)Remote WITS Jesper Cockx TU Delft

15:05 - 16:20	Session 4WITS at Salon III Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag

15:05 15m Talk		mitten: A Flexible Multimodal Proof AssistantRemote WITS Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
15:20 15m Talk		Understandable and Useful Error Messages for Liquid TypesRemote WITS Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
15:35 15m Talk		Deciding type equivalence with simple grammarsIn-Person WITS Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
15:50 15m Talk		Typechecking up to CongruenceIn-Person WITS Jad Elkhaleq Ghalayini University of Cambridge
16:05 15m Talk		À bas l’η — Coq’s troublesome η-conversionRemote WITS Meven Lennon-Bertrand Inria – LS2N, Université de Nantes

16:40 - 17:30	Session 5WITS at Salon III Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag

16:40 15m Talk		Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person WITS Matthew L. Daggitt Heriot-Watt University, Guillaume Allais University of St Andrews
16:55 15m Talk		Setting the Record Straight with SingletonsRemote WITS Reed Mullanix University of Minnesota
17:10 15m Talk		First-class pattern synonymsIn-Person WITS Tesla Zhang The Pennsylvania State University

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


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Salon III	ProLaLa Research keynote									ProLaLa Long talks #1							ProLaLa Long talks #2																																						ProLaLa Short talks								ProLaLa Long talks #3											ProLaLa Long talks #4				ProLaLa Industry keynote									ProLaLa Long talks #5						ProLaLa Long talks #6

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


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Salon III	CPP										CPP Welcome from the chairs		CPP Invited Talk												CPP				CPP Verified Data Structures and Semantics																				CPP																		CPP Semantics and Program Verification																				CPP				CPP Security and Distributed Systems																				CPP				CPP Invited Talk

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


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Salon III	CPP												CPP Invited Talk												CPP				CPP Proof Infrastructure, Rewriting and Automated Reasoning																				CPP																		CPP Formalization of Logic, Algebra and Geometry																				CPP				CPP Chairs' Report and Business Meeting								CPP				CPP Category Theory, HoTT, Number Theory

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


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Salon III					POPL Separation Logic																																						POPL Weak Memory Models																			POPL Concurrency and Parallelism																			POPL Reasoning about Probabilistic Programs and Algorithms

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


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30
Salon III					POPL Quantum Computing																																						POPL Dynamic Analysis																			POPL Metaprogramming

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


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Salon III					POPL Semantics 1																																						POPL Semantics 2																			POPL Type Theory																			POPL Synthesis

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


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Salon III	WITS Session 1																WITS Session 2																																						WITS Session 3																			WITS Session 4																			WITS Session 5

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


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Salon III	ProLaLaRemote Research keynote -- Programming Languages and Law: A Research Agenda fo ... 09:00 - 09:45									ProLaLaInPerson Legal Calculi 09:45 - 10:05							ProLaLaRemote Position Paper: LLD is All You Need 10:20 - 10:40				ProLaLaRemote Logical English as a Programming Language for the Law 10:40 - 11:00				ProLaLaRemote Introduction of PROLEG (PROlog-based LEGal reasoning support system) 11:00 - 11:20				ProLaLaRemote DPCL: a Language Template for Normative Specifications 11:20 - 11:40				ProLaLaRemote Reflections on the design and application of eFLINT 11:40 - 12:00																						ProLaLaRemote Littleton: An Educational Environment for Property Law 13:30 - 13:40		ProLaLaRemote Modeling Administrative Discretion Using Goal-Directed Answer Set Progr ... 13:40 - 13:50		ProLaLaRemote Probabilistic programming for Employment Tribunal remedies 13:50 - 14:00		ProLaLaRemote Prevalence of Expression Types in Legislative Text 14:00 - 14:10		ProLaLaRemote Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting 14:10 - 14:30				ProLaLaInPerson Cod(e)ifying The Law 14:30 - 14:50							ProLaLaRemote Stipula: a domain specific language for legal contracts 15:05 - 15:25				ProLaLaRemote Industry keynote -- What does a toolchain for legislation eventually be ... 15:25 - 16:10									ProLaLaRemote Ergo - a programming language for Smart Legal Contracts 16:10 - 16:30						ProLaLaRemote A General Library of Legal Components 16:40 - 17:00				ProLaLaRemote Overview of the CCLAW L4 project 17:00 - 17:20				ProLaLaRemote Turning Catala into a Proof Platform for the Law 17:20 - 17:40

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


Room	8:00			15			30			45			9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Salon III											CPP Chairs' report 08:50 - 09:00		CPPInPerson Coq’s vibrant ecosystem for verification engineering 09:00 - 10:00																CPPDistinguished Paper AwardRemote Specification and Verification of a Transient Stack 10:20 - 10:45					CPPRemote Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s ... 10:45 - 11:10					CPPInPerson Applying Formal Verification to Microkernel IPC at Meta 11:10 - 11:35					CPPRemote Certified Abstract Machines for Skeletal Semantics 11:35 - 12:00																							CPPRemote A Compositional Proof Framework for FRETish Requirements 13:30 - 13:55					CPPRemote Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Deri ... 13:55 - 14:20					CPPInPerson Formally Verified Superblock Scheduling 14:20 - 14:45					CPPRemote Overcoming Restraint: Composing Verification of Foreign Functions with ... 14:45 - 15:10									CPPRemote Reflection, Rewinding, and Coin-Toss in EasyCrypt 15:30 - 15:55					CPPRemote A verified algebraic representation of Cairo program execution 15:55 - 16:20					CPPInPerson Formal Verification of a Distributed Dynamic Reconfiguration Protocol 16:20 - 16:45					CPPInPerson Forward build systems, formally 16:45 - 17:10									CPPRemote The seL4 verification: the art and craft of proof and the reality of co ... 17:30 - 18:30

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


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Salon III	CPPRemote Structural Embeddings Revisited 09:00 - 10:00																CPPDistinguished Paper AwardRemote CertiStr: A Certified String Solver 10:20 - 10:45					CPPRemote Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo ... 10:45 - 11:10					CPPRemote An Extension of the Framework Types-To-Sets for Isabelle/HOL 11:10 - 11:35					CPPRemote A Drag-and-Drop Proof Tactic 11:35 - 12:00																							CPPDistinguished Paper AwardRemote Semantic cut elimination for the logic of bunched implications, formali ... 13:30 - 13:55					CPPRemote Undecidability, Incompleteness, and Completeness of Second-Order Logic ... 13:55 - 14:20					CPPRemote Formalising Lie algebras 14:20 - 14:45					CPPInPerson A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem 14:45 - 15:10									CPP Chairs' Report 15:30 - 16:10												CPPRemote Implementing a category-theoretic framework for typed abstract syntax 16:30 - 16:55					CPPRemote (Deep) Induction Rules for GADTs 16:55 - 17:20					CPPRemote On homotopy of walks and spherical maps in homotopy type theory 17:20 - 17:45					CPPRemote Windmills of the minds: an algorithm for Fermat's Two Squares Theorem 17:45 - 18:10

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


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Salon III					POPL Remote A Separation Logic for Heap Space under Garbage Collection 10:20 - 10:45					POPL Distinguished PaperRemote Simuliris: A Separation Logic Framework for Verifying Concurrent Progra ... 10:45 - 11:10					POPL Remote Concurrent Incorrectness Separation Logic 11:10 - 11:35					POPL InPerson On Incorrectness Logic and Kleene Algebra with Top and Tests 11:35 - 12:00																							POPL InPerson The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Me ... 13:30 - 13:55					POPL Remote Extending Intel-x86 Consistency and Persistency: Formalising the Semant ... 13:55 - 14:20					POPL Remote Truly Stateless, Optimal Dynamic Partial Order Reduction 14:20 - 14:45									POPL Remote Visibility Reasoning for Concurrent Snapshot Algorithms 15:05 - 15:30					POPL Remote Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Sep ... 15:30 - 15:55					POPL InPerson Static Prediction of Parallel Computation Graphs 15:55 - 16:20									POPL Remote A Separation Logic for Negative Dependence 16:40 - 17:05					POPL Remote Reasoning about “Reasoning about Reasoning”: Semantics and Contextual E ... 17:05 - 17:30

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


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45
Salon III					POPL Remote Quantum Information Effects 10:20 - 10:45					POPL InPerson Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs 10:45 - 11:10					POPL Remote A Quantum Interpretation of Separating Conjunction for Local Reasoning ... 11:10 - 11:35					POPL Remote Semantics for Variational Quantum Programming 11:35 - 12:00																							POPL Remote A Formal Foundation for Symbolic Evaluation with Merging 13:30 - 13:55					POPL InPerson Logarithm and Program Testing 13:55 - 14:20					POPL Remote Profile Inference Revisited 14:20 - 14:45									POPL InPerson Staging with Class: A Specification for Typed Template Haskell 15:05 - 15:30					POPL Remote Mœbius: Metaprogramming using Contextual Types: The Stage Where System ... 15:30 - 15:55					POPL Remote Type-Level Programming with Match Types 15:55 - 16:20

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


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Salon III					POPL Remote From Enhanced Coinduction towards Enhanced Induction 10:20 - 10:45					POPL InPerson A Fine-Grained Computational Interpretation of Girard’s Intuitionistic ... 10:45 - 11:10					POPL Remote Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Lo ... 11:10 - 11:35					POPL InPerson Layered and Object-Based Game Semantics 11:35 - 12:00																							POPL InPerson Symmetries in Reversible Programming: From Symmetric Rig Groupoids to R ... 13:30 - 13:55					POPL Remote A Relational Theory of Effects and Coeffects 13:55 - 14:20					POPL Remote Effectful Program Distancing 14:20 - 14:45									POPL InPerson A Cost-Aware Logical Framework 15:05 - 15:30					POPL Distinguished PaperRemote Formal Metatheory of Second-Order Abstract Syntax 15:30 - 15:55					POPL Distinguished PaperRemote Observational Equality: Now for Good 15:55 - 16:20									POPL Distinguished PaperInPerson Learning Formulas in Finite Variable Logics 16:40 - 17:05					POPL Distinguished PaperRemote Bottom-Up Synthesis of Recursive Functional Programs using Angelic Exec ... 17:05 - 17:30

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


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Salon III	WITSRemote CN: A Refinement Type System for C 09:00 - 09:15			WITSIn-Person Type-aware equational rewriting (discussion) 09:15 - 10:00 In-Person Multi case trees: confluence and coverage (discussion) 09:15 - 10:00 Remote Intrinsically-Typed Interpreters for Effectful and Coeffectful Language ... 09:15 - 10:00 Remote The Expression Problem and Theorem Proving (discussion) 09:15 - 10:00													WITSRemote Make Three To Throw Away: Frontiers in Homotopical Proof Assistants 10:20 - 11:05									WITSRemote The curious case of case: correct & efficient representation of case an ... 11:05 - 11:20			WITSRemote Elaborator reflection APIs (discussion) 11:20 - 12:00 In-Person Invisible arguments: language design (discussion) 11:20 - 12:00																										WITSRemote Tries that match 13:30 - 13:45			WITSRemote Gotta prove fast: building an ecosystem for effortless native compilati ... 13:45 - 14:00			WITSIn-Person Benchmarking Binding (discussion) 14:00 - 14:45 Remote Fancy module systems (discussion) 14:00 - 14:45													WITSRemote mitten: A Flexible Multimodal Proof Assistant 15:05 - 15:20			WITSRemote Understandable and Useful Error Messages for Liquid Types 15:20 - 15:35			WITSIn-Person Deciding type equivalence with simple grammars 15:35 - 15:50			WITSIn-Person Typechecking up to Congruence 15:50 - 16:05			WITSRemote À bas l’η — Coq’s troublesome η-conversion 16:05 - 16:20							WITSIn-Person Using Dependent Types at Scale: Maintaining the Agda Standard Library 16:40 - 16:55			WITSRemote Setting the Record Straight with Singletons 16:55 - 17:10			WITSIn-Person First-class pattern synonyms 17:10 - 17:25

Room information: Salon III

Program Display Configuration

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

ProLaLa

ProLaLa

ProLaLa

ProLaLa

ProLaLa

ProLaLa

ProLaLa

ProLaLa

ProLaLa

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

CPP

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

POPL

POPL

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

POPL

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

POPL

POPL

POPL

POPL

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

WITS

WITS

WITS

WITS

WITS

Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change

Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change

Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change

Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change

Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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