Program - POPL 2023

Detailed Table Session Timeline Detailed Timeline

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 15 Jan
Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30	Session #1ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond

09:00 10m Day opening		Opening comments ProLaLa Jonathan Protzenko Microsoft Research, Redmond, Denis Merigoux INRIA, Shrutarshi Basu Middlebury College
09:10 45m Keynote		Academic keynote : A Logician and Lawyer walk into a Classroom ProLaLa Scott Shapiro Yale Law School, Ruzica Piskac Yale University
09:55 25m Talk		Formal Modeling and Analysis of Legal Contracts using ContractCheck ProLaLa Alan Khoja University of Konstanz, Martin Kölbl CertiK, Stefan Leue University of Konstanz, Rüdiger Wilhelmi University of Konstanz DOI Pre-print
10:20 10m Talk		What do Relational Properties Have to Say About Legal Expert Systems ? ProLaLa Arthur Correnson École Normale Supérieure de Rennes & Saarland University

09:00 - 10:30	First SessionLAFI at Scollay Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6

09:00 5m Day opening		Opening Comments LAFI Christine Tasson Sorbonne Université — LIP6, Steven Holtzen Northeastern University
09:05 60m Keynote		Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.Boston LAFI A: Hongseok Yang KAIST; IBS
10:10 10m Talk		Exact Inference for Discrete Probabilistic Programs via Generating FunctionsParis LAFI A: Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford File Attached
10:20 10m Talk		Exact Probabilistic Inference Using Generating FunctionsBoston LAFI A: Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University, Mingshuai Chen RWTH Aachen, Joost-Pieter Katoen RWTH Aachen University File Attached

11:00 - 12:30	Session #2ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Thomas T. Hildebrandt University of Copenhagen, Jonathan Protzenko Microsoft Research, Redmond

11:00 25m Talk		Building Information Modeling Using Constraint Logic Programming (Extended Abstract)Virtual ProLaLa Joaquín Arias Universidad Rey Juan Carlos, Seppo Törmä VisuaLynk Oy, Finland, Manuel Carro IMDEA Software Institute and T.U. of Madrid (UPM), Gopal Gupta University of Texas at Dallas, USA Link to publication DOI Pre-print File Attached
11:25 25m Talk		Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming ProLaLa Chinmaya Dabral North Carolina State University, Emma Tosch Northeastern University, USA, Chris Martens Northeastern University Link to publication Pre-print File Attached
11:50 25m Talk		The Structure and Legal Interpretation of Computer ProgramsVirtual ProLaLa James Grimmelmann Cornell University File Attached
12:15 10m Talk		Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint ProLaLa Sterre Lutz Utrecht University and TNO DOI Pre-print
12:25 10m Talk		Defeasible Semantics for L4Virtual ProLaLa Guido Governatori Singapore Management University, Meng Weng Wong Singapore Management University Link to publication DOI

11:00 - 12:30	Second SessionLAFI at Scollay Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6

11:00 20m Talk		What do posterior distributions of probabilistic programs look like?Boston LAFI Mathieu Huot University of Oxford, A: Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Sam Staton University of Oxford File Attached
11:20 10m Talk		Semantics of Probabilistic Program TracesBoston LAFI Alexander K. Lew Massachusetts Institute of Technology, A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam, Vikash Mansinghka Massachusetts Institute of Technology File Attached
11:30 10m Talk		A convenient category of tracing measure kernelsBoston LAFI A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam File Attached
11:45 5m Talk		Random probability distributions as natural transformationsParis LAFI A: Victor Blanchi ENS Paris, Hugo Paquet University of Oxford File Attached
11:50 5m Talk		Static Delayed Sampling for Probabilistic Programming LanguagesParis LAFI A: Gizem Caylak KTH Royal Institute of Technology, Daniel Lundén KTH Royal Institute of Technology, Viktor Senderov Naturhistoriska riksmuseet, David Broman KTH Royal Institute of Technology
11:55 5m Talk		Denotational semantics of languages for inference: semirings, monads, and tensorsOnline LAFI Cristina Matache University of Edinburgh, A: Sean Moss University of Oxford, Sam Staton University of Oxford, Ariadne Si Suo University of Oxford
12:10 5m Talk		Separated and Shared Effects in Higher-Order LanguagesBoston LAFI A: Pedro Henrique Azevedo de Amorim Cornell University, Justin Hsu Cornell University
12:15 5m Talk		On Iteration in Discrete Probabilistic ProgrammingBoston LAFI A: Mateo Torres-Ruiz , Robin Piedeleu University of Oxford, Alexandra Silva Cornell University, Fabio Zanasi University College London File Attached
12:20 5m Talk		Bit-Blasting Probabilistic ProgramsBoston LAFI A: Poorva Garg University of California, Los Angeles, Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles File Attached
12:25 5m Talk		πMPC: Automatic Security Proofs for MPC ProtocolsBoston LAFI A: Mako P. Bates University of Vermont, Joseph P. Near University of Vermont

14:00 - 15:30	Session #3ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond, Emma Tosch Northeastern University, USA

14:00 25m Talk		Experience report: implementing a real-world, medium-sized program derived from a legislative specification ProLaLa Denis Merigoux INRIA Pre-print File Attached
14:25 25m Talk		Legal Contracts Amending in StipulaVirtual ProLaLa Cosimo Laneve University of Bologna, Alessandro Parenti University of Bologna, Giovanni Sartor University of Bologna
14:50 25m Talk		Towards an Automatic Consolidation of French LawVirtual ProLaLa Georges-André Silber Mines Paris, PSL University File Attached
15:15 10m Talk		DCR Graphs as Co-created Executable Models of the Law ProLaLa Thomas T. Hildebrandt University of Copenhagen File Attached
15:25 10m Talk		Visual Propositional Logic With yscriptVirtual ProLaLa William O'Hanley Stanford CodeX Link to publication

14:00 - 15:30	Third SessionLAFI at Scollay Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6

14:00 20m Talk		The Variable Elimination Algorithm as a Let-Term RewritingParis LAFI Thomas Ehrhard CNRS and University Paris Diderot, Claudia Faggian Université de Paris & CNRS, A: Michele Pagani IRIF - Université de Paris Cité
14:20 20m Talk		Contextual source code AD transformations for sum typesOnline LAFI Adam Paszke Google Research, A: Gordon Plotkin Google File Attached
14:45 5m Talk		Pitfalls of Full Bayesian Inference in Universal Probabilistic ProgrammingOnline LAFI A: Tim Reichelt University of Oxford, C.-H. Luke Ong University of Oxford, Tom Rainforth Department of Statistics, University of Oxford File Attached
14:50 5m Talk		∂ is for Dialectica: typing differentiable programmingOnline LAFI A: Marie Kerjean CNRS, Université Sorbonne Paris Nord, Pierre-Marie Pédrot INRIA
15:00 5m Talk		On the Reparameterisation Gradient for Non-Differentiable but Continuous ModelsBoston LAFI C.-H. Luke Ong NTU, A: Dominik Wagner University of Oxford File Attached
15:05 5m Talk		Partial Evaluation of Forward-Mode Automatic DifferentiationBoston LAFI A: Oscar Eriksson KTH Royal Institute of Technology, Viktor Palmkvist KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology
15:10 5m Talk		Distribution Theoretic Semantics for Non-Smooth Differentiable ProgrammingBoston LAFI Pedro Henrique Azevedo de Amorim Cornell University, A: Christopher Lam University of Illinois at Urbana-Champaign
15:15 5m Talk		New foundations for probabilistic separation logicBoston LAFI A: John Li Northeastern University, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University File Attached
15:20 5m Talk		Verified Reversible Programming for Verified Lossless CompressionBoston LAFI A: James Townsend University of Amsterdam, Jan-Willem Van De Meent University of Amsterdam
15:25 5m Talk		Towards type-driven data-science in Idris LAFI Ohad Kammar University of Edinburgh, Katarzyna Marek University of Edinburgh, Minh Nguyen University of Bristol, Michel Steuwer University of Edinburgh, Jacob Walters University of Edinburgh, Robert Wright The University of Edinburgh, UK

16:00 - 18:00	Session #4ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond

16:00 45m Keynote		Research keynote ProLaLa Chris Bailey University of Illinois College of Law
16:45 25m Talk		Designing an experiment for comparing user interfaces for legal formalization ProLaLa Tereza Novotná Masaryk university, Tomer Libal
17:10 10m Talk		Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as CodeVirtual ProLaLa Jason Morris File Attached
17:20 10m Talk		Formalising Criminal Law in CatalaVirtual ProLaLa Luca Arnaboldi The University of Edinburgh, David Aspinall University of Edinburgh, Ronny Bogani University of Edinburgh, Burkhard Schafer University of Edinburgh, Scott Herman Conan & Herman, Jonathan Protzenko Microsoft Research, Redmond, Ekaterina Komendantskaya Heriot-Watt University, UK, Remi Desmartin Heriot-Watt University, Yue Li Heriot-Watt University, UK Pre-print File Attached

	16:00 - 18:00	Poster SessionLAFI at Scollay Chair(s): Steven Holtzen Northeastern University

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

09:00 - 10:30	Keynote and contribution paper VMCAI at Arlington Chair(s): Michael Emmi Amazon Web Services

09:00 60m Keynote		Towards a Theoretical Understanding of Property-Directed Reachability VMCAI Sharon Shoham Tel Aviv University
10:00 30m Talk		Distributing and Parallelizing Non-canonical Loops VMCAI Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS

09:00 - 10:30	Tutorials 4ATutorialFest at Copley

09:00 90m Tutorial		Deductive Verification of Probabilistic Programs TutorialFest Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU

09:00 - 10:30	Tutorials 3ATutorialFest at Kenmore

09:00 90m Tutorial		QuickChick: Combining Random Testing and Verification in Coq TutorialFest Leonidas Lampropoulos University of Maryland, College Park

09:00 - 10:30	Tutorials 2ATutorialFest at Park

09:00 90m Tutorial		Isabelle/HOL: Foundations, Induction, and Coinduction TutorialFest Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen

09:00 - 10:30	Tutorials 1ATutorialFest at Scollay

09:00 90m Tutorial		Z3 Internals – A guide to principles, art and empirics of programming SMT solvers TutorialFest Nikolaj Bjørner Microsoft Research

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

09:00 - 10:00	Opening & Invited TalkPADL at The Loft Chair(s): Daniela Inclezan Miami University

09:00 60m Talk		Towards Declarative Content Generation for Creativity Support Tools PADL Chris Martens Northeastern University

10:00 - 10:30	ReasoningPADL at The Loft Chair(s): Anssi Yli-Jyrä Tampere University

10:00 30m Talk		Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL PADL Haya Majid Qureshi Alpen-Adria-Universität Klagenfurt, Wolfgang Faber University of Klagenfurt

11:00 - 12:30	Static AnalysisVMCAI at Arlington Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University

11:00 30m Talk		Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth VMCAI Amir Kafshdar Goharshady IST Austria, Austria, Ahmed Khaled Zaher HKUST
11:30 30m Talk		Result Invalidation for Incremental Modular Analyses VMCAI Jens Van der Plas Software Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
12:00 30m Talk		Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference VMCAI Nicolas Berthier OCamlPro, Narges Khakpour Linnaeus University

11:00 - 12:30	Tutorials 4BTutorialFest at Copley

11:00 90m Tutorial		Deductive Verification of Probabilistic Programs TutorialFest Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU

11:00 - 12:30	Tutorials 3BTutorialFest at Kenmore

11:00 90m Tutorial		QuickChick: Combining Random Testing and Verification in Coq TutorialFest Leonidas Lampropoulos University of Maryland, College Park

11:00 - 12:30	Tutorials 2BTutorialFest at Park

11:00 90m Tutorial		Isabelle/HOL: Foundations, Induction, and Coinduction TutorialFest Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen

11:00 - 12:30	Tutorials 1BTutorialFest at Scollay

11:00 90m Tutorial		Z3 Internals – A guide to principles, art and empirics of programming SMT solvers TutorialFest Nikolaj Bjørner Microsoft Research

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

11:00 - 12:30	Domain Specific LanguagesPADL at The Loft Chair(s): Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research

11:00 30m Talk		Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper) PADL Birthe van den Berg KU Leuven, Tom Schrijvers KU Leuven, Peter Dedecker KU Leuven
11:30 30m Talk		SwitchLog: A Logic Programming Language for Network Switches PADL Vaibhav Mehta Princeton University, Devon Loehr Princeton University, John Sonchack University of Pennsylvania, USA, David Walker Princeton University
12:00 30m Talk		Formalizing and Reasoning about Contracts between Agents PADL Dylan Flynn , Chasity Nadeau , Jeannine Shantz , Marcello Balduccini Saint Joseph's University, USA, Tran Cao Son New Mexico State University, Edward Griffor

	12:30 - 14:00	LunchPOPL at Statler & Grand Ballroom B

14:00 - 15:30	Keynote and best paperVMCAI at Arlington Chair(s): Michael Emmi Amazon Web Services

14:00 60m Keynote		What Can Program Analysis Say About Data Bias? VMCAI Aws Albarghouthi University of Wisconsin-Madison
15:00 30m Talk		Bayesian parameter estimation with guarantees via interval analysis and simulation VMCAI Luisa Collodi University of Florence

14:00 - 15:30	Tutorials 8ATutorialFest at Copley

14:00 90m Tutorial		Neurosymbolic Programming TutorialFest Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology

14:00 - 15:30	Tutorials 7ATutorialFest at Kenmore

14:00 90m Tutorial		RUST: Regions, Uniqueness, Ownership & Types TutorialFest James Noble Research & Programming, Tobias Wrigstad Uppsala University, Sweden Media Attached File Attached

14:00 - 15:30	Tutorials 6ATutorialFest at Park

14:00 90m Tutorial		Using a Proof Assistant to Teach PL Theory, Without the Overhead TutorialFest Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee

14:00 - 15:30	Tutorials 5ATutorialFest at Scollay

14:00 90m Tutorial		Incorrectness Logic and Under-approximation: Foundations of Bug Catching TutorialFest Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA

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

14:00 - 15:30	Applications of Answer Set Programming (I)PADL at The Loft Chair(s): Wolfgang Faber Alpen-Adria-Universität, Austria

14:00 30m Talk		Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming PADL Zesheng Xu The University of Texas at Dallas, Gopal Gupta University of Texas at Dallas, USA, Elmer Salazar The University of Texas at Dallas, Joaquín Arias Universidad Rey Juan Carlos, Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research
14:30 30m Talk		Solving Vehicle Equipment Specification Problems with Answer Set Programming PADL Raito Takeuchi Nagoya University, Mutsunori Banbara Nagoya University, Naoyuki Tamura Kobe University, JAPAN, Torsten Schaub University of Potsdam
15:00 30m Talk		Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling PADL Anssi Yli-Jyrä Tampere University, Masood Feyzbakhsh Rankooh Tampere University, Tomi Janhunen Tampere University

16:00 - 18:00	SolversVMCAI at Arlington Chair(s): Aws Albarghouthi University of Wisconsin-Madison

16:00 30m Talk		Solving Constrained Horn Clauses over Algebraic Data Types VMCAI Lucas Zavalia Florida State University Tallahassee, Lidiia Chernigovskaia , Grigory Fedyukovich Florida State University
16:30 30m Talk		Satisfiability Modulo Custom Theories in Z3 (Tool Paper) VMCAI Nikolaj Bjørner Microsoft Research, Clemens Eisenhofer , Laura Kovács TU Wien
17:00 30m Talk		CosySEL: Improving SAT Solving Using Local Symmetries VMCAI Sabrine Saouli , Souheib Baarir , Claude Dutheillet , Jo Devriendt

16:00 - 17:30	Tutorials 8BTutorialFest at Copley

16:00 90m Tutorial		Neurosymbolic Programming TutorialFest Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology

16:00 - 17:30	Tutorials 7BTutorialFest at Kenmore

16:00 90m Tutorial		RUST: Regions, Uniqueness, Ownership & Types TutorialFest James Noble Research & Programming, Tobias Wrigstad Uppsala University, Sweden Media Attached File Attached

16:00 - 17:30	Tutorials 6BTutorialFest at Park

16:00 90m Tutorial		Using a Proof Assistant to Teach PL Theory, Without the Overhead TutorialFest Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee

16:00 - 17:30	Tutorials 5BTutorialFest at Scollay

16:00 90m Tutorial		Incorrectness Logic and Under-approximation: Foundations of Bug Catching TutorialFest Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA

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

16:00 - 17:30	Applications of Answer Set Programming (II)PADL at The Loft Chair(s): Mutsunori Banbara Nagoya University

16:00 30m Talk		Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper) PADL Denise Angilica Università Della Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Jessica Zangari Università della Calabria
16:30 30m Talk		UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper) PADL Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research, Baoluo Meng GE Research, Christopher Alexander GE Research, Szabolcs Borgyos GE Research
17:00 30m Talk		Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set Programming (Application Paper) PADL Ramsha Ali University of Klagenfurt, Mohammed M. S. El-Kholany University of Klagenfurt, Martin Gebser University of Klagenfurt, Austria

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

09:00 - 10:30	Keynote and contribution paperVMCAI at Arlington Chair(s): Michael Emmi Amazon Web Services

09:00 60m Keynote		Differential Verification of Deep Neural Networks VMCAI Chao Wang University of Southern California
10:00 30m Talk		ARENA: Enhancing Abstract Refinement for Neural Network Verification VMCAI Yuyi Zhong , Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore

09:00 - 10:30	Keynote + 1 talkPEPM at Scollay Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)

09:00 60m Keynote		Fast Cryptographic Code via Partial Evaluation PEPM Adam Chlipala Massachusetts Institute of Technology
10:00 30m Talk		Towards Type Debugging using Partial Evaluation PEPM Kanae Tsushima National Institute of Informatics, Japan, Robert Glück University of Copenhagen

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

09:00 - 10:30	Session 1PLMW @ POPL at Studio 2 Chair(s): Hannah Gommerstadt Vassar College

09:00 15m Talk		Introduction PLMW @ POPL Amal Ahmed Northeastern University, USA Media Attached
09:15 45m Talk		Imagining the Reader PLMW @ POPL Benjamin C. Pierce University of Pennsylvania Media Attached File Attached
10:00 30m Social Event		Icebreaker Activity PLMW @ POPL

09:00 - 10:00	Invited TalkPADL at The Loft Chair(s): Michael Hanus Kiel University

09:00 60m Talk		Modern Macros PADL Robert Bruce Findler Northwestern University

10:00 - 10:30	DebuggingPADL at The Loft Chair(s): Steven Libby University of Portland

10:00 30m Talk		Automatic Rollback Suggestions for Incremental Datalog Evaluation PADL David Zhao The University of Sydney, Pavle Subotic Microsoft Azure, Mukund Raghothaman University of Southern California, Bernhard Scholz University of Sydney

11:00 - 12:30	Neural networks and Abstract InterpretationVMCAI at Arlington Chair(s): Grigory Fedyukovich Florida State University

11:00 15m Talk		Maximal Robust Neural Network Specifications via Oracle-guided Numerical OptimizationRecorded VMCAI Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
11:15 15m Talk		SMT-Based Modeling and Verification of Spiking Neural Networks: A Case StudyRecorded VMCAI Sumana Ghosh , Soham Banerjee , Swarup Mohalik , Ansuman Banerjee
11:30 30m Talk		A generic framework to coarse-grain stochastic reaction networks by Abstract Interpretation VMCAI Jerome Feret INRIA Paris, Albin Salazar INRIA/CNRS/ENS/PSL*
12:00 30m Talk		Sound Symbolic Execution via Abstract Interpretation and its Application to Security VMCAI Xavier Rival Inria; ENS; CNRS; PSL University, Ignacio Tiraboschi Inria, France / ENS, France, Tamara Rezk INRIA

11:00 - 12:30	3 talksPEPM at Scollay Chair(s): Casper Bach Poulsen Delft University of Technology

11:00 30m Talk		Semantic Transformation Framework for Rewriting Rules PEPM Jihee Park KAIST, Jaemin Hong KAIST, Sukyoung Ryu KAIST
11:30 30m Talk		Symbolic Execution of Hadamard-Toffoli Quantum Circuits PEPM Jacques Carette McMaster University, Gerardo Ortiz Indiana University, Amr Sabry Indiana University
12:00 30m Talk		Generating Programs for Polynomial Multiplication with Correctness Assurance PEPM Ryo Tokuda University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba

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

11:00 - 12:30	Session 2PLMW @ POPL at Studio 2 Chair(s): Michael Greenberg Stevens Institute of Technology

11:00 45m Talk		Session Types Meet Polymorphism and Dependent Types PLMW @ POPL Peter Thiemann University of Freiburg, Germany Media Attached File Attached
11:45 45m Panel		Career Trajectories in PL PLMW @ POPL Richard A. Eisenberg Jane Street, Anitha Gollamudi University of Massachusetts Lowell, Ryan Kavanagh McGill University, Joseph Tassarotti NYU, M: Michael Greenberg Stevens Institute of Technology

11:00 - 12:30	Functional (Logic) ProgrammingPADL at The Loft Chair(s): William E. Byrd University of Alabama at Birmingham, USA

11:00 30m Talk		RICE: An Optimizing Curry Compiler PADL Steven Libby University of Portland
11:30 30m Talk		Embedding Functional Logic Programming in Haskell via a Compiler Plugin PADL Kai-Oliver Prott University of Kiel, Germany, Finn Teegen University of Kiel, Germany, Jan Christiansen Flensburg University of Applied Sciences, Germany DOI File Attached
12:00 30m Talk		Program Synthesis Using Example Propagation PADL Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open University of the Netherlands, Netherlands

	12:30 - 14:00	LunchPOPL at Statler & Grand Ballroom B

14:00 - 15:30	Keynote and contribution paperVMCAI at Arlington Chair(s): Michael Emmi Amazon Web Services

14:00 60m Keynote		Verifying, Inferring and Exploiting Code Commutativity VMCAI Eric Koskinen Stevens Institute of Technology

14:00 - 15:30	Industry presentation + 1 talkPEPM at Scollay Chair(s): Sukyoung Ryu KAIST

14:00 60m Industry talk		MATLAB Coder: Partial Evaluation in Practice PEPM Denis Gurchenkov MathWorks, Fred Smith MathWorks
15:00 30m Talk		Modular Construction of Multi-sorted Free Extensions PEPM Guillaume Allais University of St Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Nachiappan Valliappan Chalmers University of Technology, Sam Lindley University of Edinburgh, Jeremy Yallop University of Cambridge File Attached

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

14:00 - 15:30	Session 3PLMW @ POPL at Studio 2 Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota

14:00 45m Talk		Anti-disciplinary: doing academic research when you like too many thingsremote presentation PLMW @ POPL Chris Martens Northeastern University Media Attached File Attached
14:45 45m Talk		How (not) to give a great research talk PLMW @ POPL Leonidas Lampropoulos University of Maryland, College Park Media Attached File Attached

14:00 - 15:30	VerificationPADL at The Loft Chair(s): Linda Brodo Università di Sassari

14:00 30m Talk		Execution Time Program Verification With Tight Bounds PADL Ana Carolina Silva FCUP, Manuel Barbosa HASLab - INESC TEC and FCUP, Mario Florido Universidade do Porto
14:30 30m Talk		From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting PADL Misaki Kojima Nagoya University, Naoki Nishida Nagoya University DOI File Attached
15:00 30m Talk		Multiple Query Satisfiability of Constrained Horn Clauses PADL Emanuele De Angelis CNR-IASI, Fabio Fioravanti University of Chieti-Pescara, Alberto Pettorossi University of Rome Tor Vergata, Italy, Maurizio Proietti CNR-IASI

16:00 - 17:30	Model CheckingVMCAI at Arlington Chair(s): Eric Koskinen Stevens Institute of Technology

16:00 15m Talk		A Pragmatic Approach to Stateful Partial Order ReductionRecorded VMCAI Berk Cirisci IRIF, University Paris Diderot and CNRS, France, Constantin Enea Ecole Polytechnique / LIX / CNRS, Azadeh Farzan University of Toronto, Suha Orhun Mutluergil Sabanci University, Turkey
16:15 15m Talk		StaticPersist : Compiler Support for PMEM ProgrammingRecorded VMCAI Sorav Bansal IIT Delhi and CompilerAI Labs
16:30 30m Talk		Compositional Verification of Stigmergic Collective Systems VMCAI Luca Di Stefano University of Gothenburg, Sweden, Frederic Lang
17:00 30m Talk		Synthesizing History and Prophecy Variables for Symbolic Model Checking VMCAI Cole Vick , Kenneth L. McMillan University of Texas at Austin

16:00 - 17:30	2 online talksPEPM at Scollay Chair(s): Edwin Brady University of St Andrews, UK

16:00 30m Talk		Efficient Embedding of Strategic Attribute Grammars via MemoizationRemote PEPM José Nuno Macedo University of Minho, Emanuel Rodrigues HASLab & INESC TEC, University of Minho, Marcos Viera University of the Republic, Uruguay, João Saraiva
16:30 30m Talk		Towards a Reflection for Effect HandlersRecorded PEPM Youyou Cong Tokyo Institute of Technology, Kenichi Asai Ochanomizu University
17:00 30m Day closing		Wrap up PEPM Jens Palsberg University of California, Los Angeles (UCLA), Edwin Brady University of St Andrews, UK

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

16:00 - 17:30	Session 4PLMW @ POPL at Studio 2 Chair(s): Robbert Krebbers Radboud University Nijmegen

16:00 45m Talk		Big Ideas in Program Synthesis PLMW @ POPL Nadia Polikarpova University of California at San Diego Media Attached File Attached
16:45 45m Talk		Care and Feeding of Advisors PLMW @ POPL Stephen Chong Harvard University Media Attached File Attached

16:00 - 17:30	Analysis and Symbolic MethodsPADL at The Loft Chair(s): Naoki Nishida Nagoya University

16:00 30m Talk		Dynamic slicing of Reaction Systems based on assertions and monitors PADL Linda Brodo Università di Sassari, Roberto Bruni University of Pisa, Moreno Falaschi Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche, University of Siena
16:30 30m Talk		Linear Algebraic Abduction with Partial Evaluation PADL Tuan Nguyen National Institute of Informatics, Katsumi Inoue NII, Chiaki Sakama Wakayama University DOI File Attached

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

	08:00 - 09:00	Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B Career Search

08:30 - 08:50	Wednesday Breakfast Session PreviewSession Previews at White Hill Chair(s): Nate Foster Cornell University

08:30 10m Talk		Automated Verification: Session Preview Session Previews Michael Greenberg Stevens Institute of Technology
08:40 10m Talk		Types I: Session Preview Session Previews Neel Krishnaswami University of Cambridge

	09:00 - 09:10	WelcomePOPL at Grand Ballroom A Chair(s): Andrew Myers Cornell University, Amal Ahmed Northeastern University, USA

09:10 - 10:15	Invited TalkPOPL at Grand Ballroom A Chair(s): Amal Ahmed Northeastern University, USA

09:10 65m Keynote		Principles of Persistent Programming POPL Viktor Vafeiadis MPI-SWS

10:20 - 10:40	Wednesday Morning Break Session PreviewSession Previews at White Hill Chair(s): Eric Campbell Cornell University

10:20 10m Talk		Security: Session Preview Session Previews Limin Jia Carnegie Mellon University
10:30 10m Talk		Synthesis I: Session Preview Session Previews Nadia Polikarpova University of California at San Diego

10:45 - 12:00	Types IPOPL at Avenue34 Chair(s): Neel Krishnaswami University of Cambridge

10:45 25m Talk		Higher-Order Leak and Deadlock Free LocksDistinguished Paper POPL Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University DOI
11:10 25m Talk		Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations POPL Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP DOI
11:35 25m Talk		Recursive Subtyping for All POPL Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI

10:45 - 12:00	Automated VerificationPOPL at Grand Ballroom A Chair(s): Michael Greenberg Stevens Institute of Technology

10:45 25m Talk		Kater: Automating Weak Memory Model Metatheory and Consistency Checking POPL Michalis Kokologiannakis MPI-SWS, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS DOI
11:10 25m Talk		Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual POPL Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg DOI
11:35 25m Talk		A Partial Order View of Message-Passing Communication Models POPL Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS DOI

	12:00 - 13:30	URM@POPL LunchDiversity, Equity and Inclusion at Grand Ballroom B

	12:00 - 13:30	LunchPOPL at Statler & Grand Ballroom B

12:40 - 13:20	Wednesday Lunch Session PreviewSession Previews at White Hill Chair(s): Chelsea Edmonds University of Cambridge

12:40 10m Talk		Logic & Decidability I: Session Preview Session Previews Zachary Kincaid Princeton University
12:50 10m Talk		Program Logics & Resources: Session Preview Session Previews Philippa Gardner Imperial College London
13:00 10m Talk		Verified Compilation: Session Preview Session Previews Deian Stefan University of California at San Diego
13:10 10m Talk		Probabilistic Inference: Session Preview Session Previews Alexandra Silva Cornell University

13:30 - 14:45	Program Logics & ResourcesPOPL at Avenue34 Chair(s): Robbert Krebbers Radboud University Nijmegen

13:30 25m Talk		A High-Level Separation Logic for Heap Space under Garbage Collection POPL Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria DOI
13:55 25m Talk		CN: Verifying Systems C Code with Separation-Logic Refinement Types POPL Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge DOI
14:20 25m Talk		Conditional Contextual Refinement POPL Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS DOI

13:30 - 14:45	Logic & Decidability IPOPL at Grand Ballroom A Chair(s): Zachary Kincaid Princeton University

13:30 25m Talk		Witnessability of Undecidable Problems POPL Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI
13:55 25m Talk		On the Expressive Power of String Constraints POPL Joel D. Day Loughborough University, Vijay Ganesh Georgia Tech, Nathan Grewal University of Waterloo, Florin Manea University of Göttingen DOI
14:20 25m Talk		A Robust Theory of Series Parallel Graphs POPL Rajeev Alur University of Pennsylvania, Caleb Stanford University of California, San Diego; University of California, Davis, Chris Watson University of Pennsylvania DOI

15:10 - 16:25	SecurityPOPL at Avenue34 Chair(s): Benjamin C. Pierce University of Pennsylvania

15:10 25m Talk		MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code POPL Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San Diego DOI
15:35 25m Talk		Reconciling Shannon and Scott with a Lattice of Computable Information POPL Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime Video Link to publication DOI Pre-print
16:00 25m Talk		A Core Calculus for Equational Proofs of Cryptographic Protocols POPL Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell University DOI

15:10 - 16:25	Synthesis IPOPL at Grand Ballroom A Chair(s): Nadia Polikarpova University of California at San Diego

15:10 25m Talk		Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions POPL Woosuk Lee Hanyang University, Hangyeol Cho Hanyang University DOI
15:35 25m Talk		FlashFill++: Scaling Programming by Example by Cutting to the Chase POPL José Pablo Cambronero Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Perelman Microsoft, Arjun Radhakrishna Microsoft, Clint Simon Microsoft, Ashish Tiwari Microsoft DOI
16:00 25m Talk		Unrealizability Logic POPL Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison DOI

16:45 - 18:00	Verified CompilationPOPL at Avenue34 Chair(s): Ralf Jung ETH Zürich

16:45 25m Talk		DimSum: A Decentralized Approach to Multi-language Semantics and VerificationDistinguished Paper POPL Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Youngju Song Seoul National University; MPI-SWS, Emanuele D’Osualdo MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Deepak Garg MPI-SWS, Derek Dreyer MPI-SWS DOI
17:10 25m Talk		Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler POPL Aurèle Barrière University of Rennes; Inria; CNRS; IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA, David Pichardie Meta DOI Pre-print
17:35 25m Talk		Dargent: A Silver Bullet for Verified Data Layout Refinement POPL Zilin Chen UNSW, Ambroise Lafont University of Cambridge, Liam O'Connor University of Edinburgh, Gabriele Keller Utrecht University, Craig McLaughlin UNSW, Vincent Jackson University of Melbourne, Christine Rizkallah University of Melbourne DOI

16:45 - 18:00	Probabilistic InferencePOPL at Grand Ballroom A Chair(s): Steven Holtzen Northeastern University

16:45 25m Talk		Affine Monads and Lazy Structures for Bayesian Programming POPL Swaraj Dash University of Oxford, Younesse Kaddar University of Oxford, Hugo Paquet University of Oxford, Sam Staton University of Oxford DOI
17:10 25m Talk		Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic InferenceVirtual POPL Jianlin Li University of Waterloo, Leni Ven University of Waterloo, Pengyuan Shi University of Waterloo, Yizhou Zhang University of Waterloo DOI
17:35 25m Talk		Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference POPL Wonyeol Lee Stanford University, Xavier Rival Inria; ENS; CNRS; PSL University, Hongseok Yang KAIST; IBS DOI

18:00 - 21:00	ReceptionPOPL at Foyer

18:00 3h Social Event		Reception POPL

18:00 - 19:30	SRC PosterStudent Research Competition at Grand Ballroom A Chair(s): Jeehoon Kang KAIST, Danfeng Zhang Pennsylvania State University

18:00 90m Talk		Zydeco: A Stack-Based Call-By-Push-Value Language Student Research Competition Yuchen Jiang University of Michigan, Runze Xue CSE Department at the University of Michigan
18:00 90m Talk		HasChor: Choreographic Programming in Haskell Student Research Competition Gan Shen University of California, Santa Cruz, USA
18:00 90m Talk		Towards Synthesis in Superposition Student Research Competition Petra Hozzová TU Wien
18:00 90m Talk		A Formalization of Observational Equivalence in Message Passing Protocols Student Research Competition Nathan Liittschwager University of California, Santa Cruz
18:00 90m Talk		On the metatheory of IRs and the CPS-calculus Student Research Competition Paulo Torrens University of Kent
18:00 90m Talk		Scalable Synthesis of Regular Expressions From Only Positive Examples Student Research Competition Elizaveta Pertseva UCSD, Mark Barbone UCSD
18:00 90m Talk		Evaluating Soundness of a Gradual Verifier with Property Based Testing Student Research Competition Jan-Paul Ramos-Davila Cornell University
18:00 90m Talk		A mechanized model for logical clocks Student Research Competition Jonathan Castello UC Santa Cruz
18:00 90m Talk		Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness Student Research Competition Julia Turcotti MIT-CSAIL
18:00 90m Talk		Synthesizing Vectorized Code via Verified Lifting Student Research Competition Jeremy Ferguson University of California-Berkeley
18:00 90m Talk		Citrus: A Dependently Typed Framework for Pulse-Based Logic Student Research Competition Harlan Kringen UC Santa Barbara, Ben Hardekopf University of California at Santa Barbara
18:00 90m Talk		Neko: A quantum map-filter-reduce programming language Student Research Competition Elton Pinto Georgia Institute of Technology
18:00 90m Talk		Compiling and Running High-level Quantum Programs Student Research Competition Hristo Venev INSAIT
18:00 90m Talk		Trace-Guided Inductive Synthesis of Recursive Functional Programs Student Research Competition Yongwei Yuan Purdue University

18:10 - 18:30	Wednesday Evening Session PreviewSession Previews at White Hill Chair(s): Xuejing Huang University of Hong Kong

18:10 10m Talk		Synthesis II: Session Preview Session Previews Nate Foster Cornell University
18:20 10m Talk		Semantics I: Session Preview Session Previews Ugo Dal Lago University of Bologna; Inria

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

	08:00 - 09:00	Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B Junior Faculty

08:20 - 08:50	Thursday Breakfast Session PreviewSession Previews at White Hill Chair(s): Eric Campbell Cornell University

08:20 10m Talk		Program Analysis & Parsing: Session Preview Session Previews David Pichardie Meta
08:30 10m Talk		Resource Analysis: Session Preview Session Previews Xavier Rival Inria; ENS; CNRS; PSL University
08:40 10m Talk		Automatic Differentiation: Session Preview Session Previews Sasa Misailovic University of Illinois at Urbana-Champaign

09:00 - 10:00	Panel: Next 50 Years of POPLPOPL at Grand Ballroom A Chair(s): Andrew Myers Cornell University

09:00 60m Panel		Panel: Next 50 Years of POPL POPL M: Derek Dreyer MPI-SWS, P: Michael Carbin Massachusetts Institute of Technology, P: Nate Foster Cornell University, P: Xavier Leroy Collège de France, P: Benjamin C. Pierce University of Pennsylvania, P: Nadia Polikarpova University of California at San Diego, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University

10:05 - 10:15	Thursday Morning Break Session PreviewSession Previews at White Hill Chair(s): Nate Foster Cornell University

10:05 10m Talk		Type Theory: Session Preview Session Previews Max S. New University of Michigan

10:20 - 12:00	Semantics IPOPL at Avenue34 Chair(s): Neel Krishnaswami University of Cambridge

10:20 25m Talk		A Type-Based Approach to Divide-and-Conquer Recursion in Coq POPL Pedro da Costa Abreu Junior Purdue University, Benjamin Delaware Purdue University, Alex Hubers University of Iowa, Christa Jenkins University of Iowa, J. Garrett Morris University of Iowa, Aaron Stump University of Iowa DOI
10:45 25m Talk		Elements of Quantitative RewritingVirtual POPL Francesco Gavazzo University of Pisa, Cecilia Di Florio University of Bologna DOI
11:10 25m Talk		The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding POPL Simon Castellan University of Rennes; Inria; CNRS; IRISA, Pierre Clairambault Université Aix-Marseille; Université de Toulon; CNRS; LIS DOI
11:35 25m Talk		Deconstructing the Calculus of Relations with Tape Diagrams POPL Filippo Bonchi University of Pisa, Alessandro Di Giorgio University of Pisa, Alessio Santamaria University of Pisa; University of Sussex DOI

10:20 - 12:00	Synthesis IIPOPL at Grand Ballroom A Chair(s): Benjamin Delaware Purdue University

10:20 25m Talk		babble: Learning Better Abstractions with E-Graphs and Anti-unification POPL David Cao University of California at San Diego, Rose Kunkel University of California at San Diego, Chandrakana Nandi Certora, Max Willsey University of Washington, Zachary Tatlock University of Washington, Nadia Polikarpova University of California at San Diego DOI Pre-print
10:45 25m Talk		Combining Functional and Automata Synthesis to Discover Causal Reactive Programs POPL Ria Das Stanford University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Basis; Columbia University DOI
11:10 25m Talk		Comparative Synthesis: Learning Near-Optimal Network Designs by Query POPL Yanjun Wang Amazon Web Services, USA, Zixuan Li Purdue University, Chuan Jiang Purdue University, Xiaokang Qiu Purdue University, Sanjay Rao Purdue University DOI
11:35 25m Talk		Top-Down Synthesis for Library Learning POPL Maddy Bowers Massachusetts Institute of Technology, Theo X. Olausson Massachusetts Institute of Technology, Lionel Wong Massachusetts Institute of Technology, Gabriel Grand Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Kevin Ellis Cornell University, Armando Solar-Lezama Massachusetts Institute of Technology DOI Pre-print

	12:00 - 13:30	LunchPOPL at Statler & Grand Ballroom B

13:00 - 13:20	Thursday Lunch Session PreviewSession Previews at White Hill Chair(s): Gabe Grand

13:00 10m Talk		Logic & Decidability II: Session Preview Session Previews Caleb Stanford University of California, San Diego; University of California, Davis
13:10 10m Talk		Types II: Session Preview Session Previews Benjamin C. Pierce University of Pennsylvania

13:30 - 14:45	Resource AnalysisPOPL at Avenue34 Chair(s): Robert Harper Carnegie Mellon University

13:30 25m Talk		Probabilistic Resource-Aware Session Types POPL Ankush Das Amazon, Di Wang Peking University, Jan Hoffmann Carnegie Mellon University DOI
13:55 25m Talk		A Calculus for Amortized Expected Runtimes POPL Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU, Lena Verscht RWTH Aachen University DOI
14:20 25m Talk		A General Noninterference Policy for Polynomial Time POPL Emmanuel Hainry Université de Lorraine; CNRS; Inria; LORIA, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA DOI

13:30 - 14:45	Program Analysis & ParsingPOPL at Grand Ballroom A Chair(s): David Pichardie Meta

13:30 25m Talk		SSA Translation Is an Abstract InterpretationDistinguished Paper POPL Matthieu Lemerre Université Paris-Saclay - CEA LIST DOI Pre-print
13:55 25m Talk		Dynamic Race Detection with O(1) SamplesDistinguished Paper POPL Mosaad Al Thokair University of Illinois at Urbana-Champaign, Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print
14:20 25m Talk		Statically Resolvable Ambiguity POPL Viktor Palmkvist KTH Royal Institute of Technology, Elias Castegren Uppsala University, Philipp Haller KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology DOI

13:30 - 15:00	SRC PresentationStudent Research Competition at White Hill

13:30 15m Talk		Scalable Synthesis of Regular Expressions From Only Positive Examples Student Research Competition Elizaveta Pertseva UCSD, Mark Barbone UCSD
13:45 15m Talk		Synthesizing Vectorized Code via Verified Lifting Student Research Competition Jeremy Ferguson University of California-Berkeley
14:00 15m Talk		Evaluating Soundness of a Gradual Verifier with Property Based Testing Student Research Competition Jan-Paul Ramos-Davila Cornell University
14:15 15m Talk		On the metatheory of IRs and the CPS-calculus Student Research Competition Paulo Torrens University of Kent
14:30 15m Talk		Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness Student Research Competition Julia Turcotti MIT-CSAIL
14:45 15m Talk		Compiling and Running High-level Quantum Programs Student Research Competition Hristo Venev INSAIT

15:10 - 16:25	Type TheoryPOPL at Avenue34 Chair(s): Brigitte Pientka McGill University

15:10 25m Talk		Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper POPL Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen DOI
15:35 25m Talk		An Order-Theoretic Analysis of Universe Polymorphism POPL Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of Minnesota DOI
16:00 25m Talk		Impredicative Observational Equality POPL Loïc Pujet Inria, Nicolas Tabareau Inria DOI

15:10 - 16:25	Automatic DifferentiationPOPL at Grand Ballroom A Chair(s): Ningning Xie University of Toronto

15:10 25m Talk		You Only Linearize Once: Tangents Transpose to Gradients POPL Alexey Radul Google Research, Adam Paszke Google Research, Roy Frostig Google Research, Matthew J. Johnson Google Research, Dougal Maclaurin Google Research DOI
15:35 25m Talk		Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations POPL Tom Smeding Utrecht University, Matthijs Vákár Utrecht University DOI Pre-print
16:00 25m Talk		ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsDistinguished Paper POPL Alexander K. Lew Massachusetts Institute of Technology, Mathieu Huot University of Oxford, Sam Staton University of Oxford, Vikash K. Mansinghka Massachusetts Institute of Technology DOI Pre-print

	16:45 - 18:00	POPL Business MeetingPOPL at Grand Ballroom A

18:10 - 18:30	Thursday Evening Session PreviewSession Previews at White Hill Chair(s): Alexandra E. Michael University of California at San Diego; University of Washington

18:10 10m Talk		Semantics & Effects: Session Preview Session Previews Andrew K. Hirsch University at Buffalo, SUNY
18:20 10m Talk		Logic Programming: Session Preview Session Previews Cody Roux AWS

	19:30 - 21:30	W@POPL DinnerDiversity, Equity and Inclusion at W@POPL Dinner

	20:00 - 23:00	URM@POPL Board Game NightDiversity, Equity and Inclusion at Game Night

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

	08:00 - 09:00	Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B SIGPLAN-M

08:30 - 08:50	Friday Breakfast Session PreviewSession Previews at White Hill Chair(s): Alexandre Moine Inria

08:30 10m Talk		Formal Methods in Compilation & Implementation: Session Preview Session Previews Arjun Guha Northeastern University and Roblox Research
08:40 10m Talk		Quantum Computing: Session Preview Session Previews Jens Palsberg University of California, Los Angeles (UCLA)

09:00 - 10:15	Types IIPOPL at Avenue34 Chair(s): Alan Jeffrey Roblox

09:00 25m Talk		A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ POPL Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania DOI
09:25 25m Talk		Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations POPL Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI
09:50 25m Talk		Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework POPL Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France DOI

09:00 - 10:15	Logic & Decidability IIPOPL at Square Chair(s): Joost-Pieter Katoen RWTH Aachen University

09:00 25m Talk		When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic POPL Zachary Kincaid Princeton University, Nicolas Koh Princeton University, Shaowei Zhu Princeton University DOI
09:25 25m Talk		Higher-Order MSL Horn Constraints POPL Jerome Jochems University of Bristol, Eddie Jones University of Bristol, Steven Ramsay University of Bristol DOI
09:50 25m Talk		Fast Coalgebraic Bisimilarity Minimization POPL Jules Jacobs Radboud University Nijmegen, Thorsten Wissmann Radboud University Nijmegen DOI Pre-print

10:20 - 10:40	Friday Morning Break Session PreviewSession Previews at White Hill Chair(s): Neea Rusch Augusta University

10:20 10m Talk		Concurrency & Linearizability: Session Preview Session Previews Chung-Kil Hur Seoul National University
10:30 10m Talk		Algorithmic Verification Session Previews Umang Mathur National University of Singapore

10:45 - 12:00	Semantics & EffectsPOPL at Avenue34 Chair(s): Stephanie Balzer Carnegie Mellon University

10:45 25m Talk		Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice POPL Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University DOI
11:10 25m Talk		Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq POPL Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of Pennsylvania DOI
11:35 25m Talk		Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded POPL Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology DOI Pre-print

10:45 - 12:00	Quantum ComputingPOPL at Square Chair(s): Ugo Dal Lago University of Bologna; Inria

10:45 25m Talk		Qunity: A Unified Language for Quantum and Classical Computing POPL Finn Voichick University of Maryland, Liyi Li University of Maryland, Robert Rand University of Chicago, Michael Hicks University of Maryland; Amazon DOI Pre-print
11:10 25m Talk		Proto-Quipper with Dynamic LiftingVirtual POPL Peng Fu Dalhousie University, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University DOI
11:35 25m Talk		CoqQ: Foundational Verification of Quantum ProgramsVirtual POPL Li Zhou MPI-SP; Institute of Software at Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Pierre-Yves Strub Meta, Junyi Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University DOI

	12:00 - 13:30	LGBTQ@POPL LunchDiversity, Equity and Inclusion at Hancock Room

	12:00 - 13:30	LunchPOPL at Statler & Grand Ballroom B

13:00 - 13:20	Friday Lunch Session PreviewSession Previews at White Hill

13:00 10m Talk		Relational & Automated Verification: Session Preview Session Previews Eric Campbell Cornell University
13:10 10m Talk		Semantics II: Session Preview Session Previews Robert Atkey University of Strathclyde

13:30 - 14:45	Formal Methods in Compilation & ImplementationPOPL at Avenue34 Chair(s): Lindsey Kuper University of California at Santa Cruz

13:30 25m Talk		Tail Recursion Modulo Context: An Equational Approach POPL Daan Leijen Microsoft Research, Anton Lorenzen University of Edinburgh DOI
13:55 25m Talk		Taking Back Control in an Intermediate Representation for GPU Computing POPL Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; Google DOI
14:20 25m Talk		Executing Microservice Applications on Serverless, Correctly POPL Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of Pennsylvania DOI

13:30 - 14:45	Logic ProgrammingPOPL at Square Chair(s): Marco Patrignani University of Trento

13:30 25m Talk		Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationDistinguished Paper POPL Hiroshi Unno University of Tsukuba; RIKEN AIP, Tachio Terauchi Waseda University, Yu Gu University of Tsukuba, Eric Koskinen Stevens Institute of Technology DOI
13:55 25m Talk		Optimal CHC Solving via Termination Proofs POPL Yu Gu University of Tsukuba, Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP DOI
14:20 25m Talk		From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems POPL Aaron Bembenek Harvard University, Michael Greenberg Stevens Institute of Technology, Stephen Chong Harvard University DOI Pre-print

15:10 - 16:25	Concurrency & LinearizabilityPOPL at Avenue34 Chair(s): Tej Chajed VMware Research

15:10 25m Talk		An Operational Approach to Library Abstraction under Relaxed Memory Concurrency POPL Abhishek Kr Singh Tel Aviv University, Ori Lahav Tel Aviv University DOI
15:35 25m Talk		The Path to Durable Linearizability POPL Emanuele D’Osualdo MPI-SWS, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS DOI
16:00 25m Talk		A Compositional Theory of Linearizability POPL Arthur Oliveira Vale Yale University, Zhong Shao Yale University, Yixuan Chen Yale University DOI

15:10 - 16:25	Algorithmic VerificationPOPL at Square Chair(s): Umang Mathur National University of Singapore

15:10 25m Talk		The Fine-Grained Complexity of CFL Reachability POPL Paraschos Koutris University of Wisconsin-Madison, Shaleen Deep Microsoft DOI
15:35 25m Talk		Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming POPL Yuanbo Li Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, Thomas Reps University of Wisconsin-Madison DOI
16:00 25m Talk		Context-Bounded Verification of Context-Free Specifications POPL Pascal Baumann MPI-SWS, Moses Ganardi MPI-SWS, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam MPI-SWS, Georg Zetzsche MPI-SWS DOI

16:45 - 18:00	Semantics IIPOPL at Avenue34 Chair(s): Max S. New University of Michigan

16:45 25m Talk		Locally Nameless Sets POPL Andrew M. Pitts University of Cambridge DOI Pre-print
17:10 25m Talk		Why Are Proofs Relevant in Proof-Relevant Models? POPL Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds DOI
17:35 25m Talk		Towards a Higher-Order Mathematical Operational Semantics POPL Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg DOI Pre-print

16:45 - 18:00	Relational & Automated VerificationPOPL at Square Chair(s): Christoph Matheja DTU

16:45 25m Talk		An Algebra of Alignment for Relational Verification POPL Timos Antonopoulos Yale University, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Ramana Nagasamudram Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Minh Ngo Stevens Institute of Technology DOI
17:10 25m Talk		Grisette: Symbolic Compilation as a Functional Programming Library POPL Sirui Lu University of Washington, Rastislav Bodík Google Research DOI
17:35 25m Talk		HFL(Z) Validity Checking for Automated Program Verification POPL Naoki Kobayashi University of Tokyo, Kento Tanahashi University of Tokyo, Ryosuke Sato University of Tokyo, Takeshi Tsukada Chiba University DOI

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

09:00 - 10:30	Session 1PriSC at Park Chair(s): Marco Guarnieri IMDEA Software Institute

09:00 5m Day opening		Introduction PriSC
09:05 60m Keynote		Semantic Intermediate Representations for Sound Language Interoperability PriSC Amal Ahmed Northeastern University, USA Pre-print
10:05 25m Talk		Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers PriSC Farzaneh Derakhshan Carnegie Mellon University, Zichao Zhang Carnegie Mellon University, Amit Vasudevan Carnegie Mellon University, Limin Jia Carnegie Mellon University File Attached

09:00 - 10:30	Session 1CoqPL at Scollay

09:00 60m Talk		Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) CoqPL Samuel Gruetter Massachusetts Institute of Technology
10:00 30m Talk		Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching CoqPL Xinyi Wan Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University File Attached

11:00 - 12:30	Session 2PriSC at Park Chair(s): Cătălin Hriţcu MPI-SP

11:00 25m Talk		Automated Learning and Verification of Embedded Security Architectures PriSC Matteo Busi University Ca' Foscari, Venice, Riccardo Focardi University Ca' Foscari, Venice, Flaminia L. Luccio University Ca' Foscari, Venice File Attached
11:25 25m Talk		pi_RA: A pi-calculus for verifying protocols that use remote attestation PriSC Emiel Lanckriet KU Leuven, Matteo Busi University Ca' Foscari, Venice, Dominique Devriese KU Leuven File Attached
11:50 25m Talk		Robust Constant-Time Cryptography PriSC Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Max Planck Institute for Security and Privacy (MPI-SP), Sunjay Cauligi University of California at San Diego, USA, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego Pre-print
12:15 15m Talk		Short Talk: Generalising secure compilation criteria PriSC Emiel Lanckriet KU Leuven

11:00 - 12:30	Session 2CoqPL at Scollay

11:00 30m Talk		Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation CoqPL Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Adam Chlipala Massachusetts Institute of Technology File Attached
11:30 30m Talk		Integrating graphical proofs in Coq CoqPL Pablo Donato Ecole polytechnique, Benjamin Werner LIX, IPP, Kaustuv Chaudhuri INRIA & LIX, IPP File Attached
12:00 30m Talk		Towards Formally Verified Path ORAM in Coq CoqPL Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign File Attached

	12:00 - 13:30	LunchPOPL at Avenue34

14:00 - 15:30	Session 3PriSC at Park Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay

14:00 25m Talk		Blame-Preserving Secure Compilation PriSC Marco Patrignani University of Trento, Matthis Kruse CISPA Helmholtz Center for Information Security Pre-print
14:25 25m Talk		*Securely Compiling F Programs With IO and Then Linking Them Against Weakly-Typed InterfacesRecorded** PriSC Cezar-Constantin Andrici MPI-SP, Cătălin Hriţcu MPI-SP, Théo Winterhalter INRIA Saclay Pre-print File Attached
14:50 25m Talk		SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine PriSC Jérémy Thibault MPI-SP, Arthur Azevedo de Amorim Boston University, Roberto Blanco MPI-SP, Aina Linn Georges Aarhus University, Cătălin Hriţcu MPI-SP, Andrew Tolmach Portland State University Pre-print Media Attached File Attached

14:00 - 15:30	Session 3CoqPL at Scollay

14:00 30m Talk		Verified Differential Privacy for Finite Computers CoqPL Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University File Attached
14:30 30m Talk		Formalizing Monoidal Categories and Actions for Syntax with Binders CoqPL Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft File Attached
15:00 30m Talk		Certifying Complexity Analysis CoqPL Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS File Attached

16:00 - 17:30	Session 4PriSC at Park Chair(s): Matteo Busi University Ca' Foscari, Venice

16:00 25m Talk		Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers PriSC Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego File Attached
16:25 25m Talk		FaJITa: Verifying Optimizations on Just-In-Time Programs PriSC David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMU Pre-print File Attached
16:50 25m Talk		Universally Composable Security for Program Partitioning PriSC Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell University File Attached

16:00 - 17:30	Session with the Coq development teamCoqPL at Scollay

16:00 45m Talk		Session with the Coq Development Team CoqPL Yves Bertot INRIA, Maxime Dénès Inria

POPL 2023 Program

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

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

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

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

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

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

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

POPL 2023 Program

Switch Program View

Program Display Configuration

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

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

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

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

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

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

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

Get Calendar (iCal)

Information for Participants

Information for Participants

Information for Participants

Information for Participants

Information for Participants

Information for Participants

Information for Participants

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

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

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

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

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

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

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