Kelvin Lecture - POPL 2024

VenueInstitution of Engineering and Technology

Room nameKelvin Lecture

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect 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 14 Jan
Displayed time zone: London change

09:00 - 10:30	First SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University

09:00 10m Talk		Opening Remarks LAFI
09:10 60m Keynote		Hong Ge: Bayesian inference using probabilistic programming LAFI Hong Ge University of Cambridge
10:10 20m Talk		Basis Talk LAFI

11:00 - 12:30	Second SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University

11:00 10m Talk		A Tree Sampler for Bounded Context-Free Languages LAFI Breandan Considine McGill University File Attached
11:10 10m Talk		A Multi-language Approach to Probabilistic Program Inference LAFI Sam Stites Northeastern University, Steven Holtzen Northeastern University
11:20 10m Talk		Belief Programming in Partially Observable Probabilistic Environments LAFI Tobias Gürtler Saarland University, Saarland Informatics Campus, Benjamin Lucien Kaminski Saarland University; University College London
11:30 10m Talk		Homomorphic Reverse Differentiation of IterationOnline LAFI Fernando Lucatelli Nunes Utrecht University, Gordon Plotkin Google, Matthijs Vákár Utrecht University File Attached
11:40 10m Talk		MultiSPPL: extending SPPL with multivariate leaf nodes LAFI Matin Ghavami Massachusetts Institute of Technology, Mathieu Huot MIT, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology
11:50 10m Talk		Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators LAFI McCoy Reynolds Becker MIT, Mathieu Huot MIT, Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology
12:00 10m Talk		Sparse Differentiation in Computer Graphics LAFI Kevin Mu University of Washington, Jesse Michel Massachusetts Institute of Technology, William S. Moses Massachusetts Institute of Technology, Shoaib Kamil Adobe Research, Zachary Tatlock University of Washington, Alec Jacobson University of Toronto, Jonathan Ragan-Kelley Massachusetts Institute of Technology
12:10 10m Talk		A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming LAFI Maria-Nicoleta Craciun University of Oxford, C.-H. Luke Ong NTU, Hugo Paquet LIPN, Université Sorbonne Paris Nord, Sam Staton University of Oxford
12:20 10m Talk		Effective Sequential Monte Carlo for Language Model Probabilistic Programs LAFI Alexander K. Lew Massachusetts Institute of Technology, Tan Zhi-Xuan Massachusetts Institute of Technology, Gabriel Grand Massachusetts Institute of Technology, Jacob Andreas MIT, Vikash K. Mansinghka Massachusetts Institute of Technology

14:00 - 15:30	Third SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University

14:00 10m Talk		Effect Handlers for Choice-Based Learning LAFI Gordon Plotkin Google, Ningning Xie University of Toronto File Attached
14:10 10m Talk		Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions LAFI Fabian Zaiser University of Oxford, Andrzej Murawski University of Oxford, C.-H. Luke Ong NTU File Attached
14:20 10m Talk		JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax LAFI Xianda Sun University of Cambridge, Philipp Gabler Independent researcher, Andrew Thomas University of Cambridge, Hong Ge University of Cambridge
14:30 10m Talk		Mixture Languages LAFI Oliver Richardson Cornell University, Jialu Bao Cornell University File Attached
14:40 10m Talk		Structured Tensor Algebra for Efficient Discrete Probabilistic Inference LAFI Amir Shaikhha University of Edinburgh
14:50 10m Talk		Towards a Categorical Model of the Lilac Separation Logic LAFI John Li Northeastern University, Jon Aytac Sandia National Laboratories, Philip Johnson-Freyd Sandia National Laboratories, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University File Attached
15:00 10m Talk		Toward Probabilistic Coarse-to-Fine Program Synthesis LAFI Maddy Bowers Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology
15:10 10m Talk		Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial SolvingOnline LAFI Peixin Wang University of Oxford, Hongfei Fu Shanghai Jiao Tong University, Tengshun Yang SKLCS, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Guanyan Li University of Oxford, C.-H. Luke Ong NTU
15:20 10m Talk		Abstract Interpretation for Automatic DifferentiationOnline LAFI Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign; Zhejiang University, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Sasa Misailovic University of Illinois at Urbana-Champaign

	16:00 - 17:30	Poster and Interactive SessionLAFI at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University, Matthijs Vákár Utrecht University Poster session taking place in the same room as the workshop.

Mon 15 Jan
Displayed time zone: London change

09:00 - 10:30	Logic and BeyondCPP at Kelvin Lecture Chair(s): Sandrine Blazy University of Rennes

09:00 60m Keynote		Under-approximation for Scalable Bug Detection CPP Azalea Raad Imperial College London
10:00 30m Talk		A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic CPP Ian Shillito Australian National University, Dominik Kirst Ben-Gurion University of the Negev Pre-print

11:00 - 12:30	Compiler / Program VerificationCPP at Kelvin Lecture Chair(s): Vadim Zaliva University of Cambridge, UK

11:00 30m Talk		The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography CPP Philipp G. Haselwarter Aarhus University, Benjamin Salling Hvass Aarhus University, Lasse Letager Hansen Aarhus University, Théo Winterhalter INRIA Saclay, Cătălin Hriţcu MPI-SP, Bas Spitters Aarhus University Pre-print File Attached
11:30 30m Talk		UTC time, formally verified CPP Ana de Almeida Borges University of Barcelona and Formal Vindications S.L., Mireia González Bedmar University of Barcelona and Formal Vindications S.L., Juan Conejero Rodríguez University of Barcelona and Formal Vindications S.L., Eduardo Hermo Reyes University of Barcelona and Formal Vindications S.L., Joaquim Casals Buñuel University of Barcelona and Formal Vindications S.L., Joost J. Joosten University of Barcelona
12:00 30m Talk		VCFloat2: Floating-point error analysis in Coq CPP Andrew W. Appel Princeton University, Ariel E. Kellison Cornell University Pre-print

14:00 - 15:30	Isabelle, PVSCPP at Kelvin Lecture Chair(s): Dmitriy Traytel University of Copenhagen

14:00 30m Talk		A Temporal Differential Dynamic Logic Formal Embeddingremote presentation CPP Lauren White NASA, Laura Titolo AMA/NASA LaRC, J Tanner Slagel NASA, Cesar Munoz NASA
14:30 30m Talk		Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemmadistinguished paper CPP Chelsea Edmonds University of Sheffield, Lawrence Paulson University of Cambridge Pre-print
15:00 30m Talk		Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs CPP Nao Hirokawa Japan Advanced Institute of Science and Technology, Dohan Kim University of Innsbruck, Kiraku Shintani Japan Advanced Institute of Science and Technology, René Thiemann University of Innsbruck

16:00 - 17:30	Formalizing MathematicsCPP at Kelvin Lecture Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota

16:00 30m Talk		A Formalization of Complete Discrete Valuation Rings and Local Fields CPP María Inés de Frutos-Fernández Universidad Autónoma de Madrid, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Université Jean Monnet Saint-Étienne Pre-print
16:30 30m Talk		Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture CPP Siddhartha Gadgil Indian Institute of Science, Anand Rao Tadipatri Indian Institute of Science Education and Research
17:00 30m Talk		Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Argumentsremote presentation CPP Joseph Eremondi University of Regina Pre-print

17:35 - 18:30	Business MeetingCPP at Kelvin Lecture

17:35 55m Meeting		Business Meeting CPP

Tue 16 Jan
Displayed time zone: London change

09:00 - 10:30	Interactive Proof Development CPP at Kelvin Lecture Chair(s): Brigitte Pientka McGill University

09:00 60m Keynote		Improved Assistance for Interactive Proof CPP Cezary Kaliszyk University of Innsbruck
10:00 30m Talk		Martin-Löf à la Coqdistinguished paper CPP Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand University of Cambridge, Kenji Maillard INRIA, Pierre-Marie Pédrot INRIA, Loïc Pujet Stockholm University

11:00 - 12:30	Formalizations of Category TheoryCPP at Kelvin Lecture Chair(s): Robert Atkey University of Strathclyde

11:00 30m Talk		Displayed Monoidal Categories for the Semantics of Linear Logic CPP Benedikt Ahrens Delft University of Technology, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Niels van der Weide Radboud University, Kobe Wullaert Delft University of Technology
11:30 30m Talk		Univalent Double Categories CPP Niels van der Weide Radboud University, Nima Rasekh Max Planck Institute for Mathematics, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University
12:00 30m Talk		Formalizing the ∞-categorical Yoneda lemma CPP Nikolai Kudasov Innopolis University, Emily Riehl Johns Hopkins University, Jonathan Weinberger Johns Hopkins University Link to publication DOI Pre-print

14:00 - 15:30	Mechanized separation logicCPP at Kelvin Lecture Chair(s): Amin Timany Aarhus University

14:00 30m Talk		Compositional Verification of Concurrent C Programs with Search Structure Templates CPP Duc-Than Nguyen University of Illinois at Chicago, Lennart Beringer Princeton University, William Mansky University of Illinois Chicago, Shengyi Wang Princeton University, USA Pre-print
14:30 30m Talk		Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logicdistinguished paper CPP Qiyuan Zhao National University of Singapore, George Pîrlea National University of Singapore, Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore, Ilya Sergey National University of Singapore Pre-print
15:00 30m Talk		Unification for Subformula Linking under Quantifiers CPP Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen Pre-print

16:00 - 17:30	Verified CompilationCPP at Kelvin Lecture Chair(s): Arthur Charguéraud Inria

16:00 30m Talk		Lean Formalization of Extended Regular Expression Matching with Lookarounds CPP Ekaterina Zhuchko Tallinn University of Technology, Margus Veanes Microsoft Research, Gabriel Ebner Microsoft Research
16:30 30m Talk		Memory simulations, security and optimization in a verified compiler CPP David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
17:00 30m Talk		PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams CPP Clément Chavanon INRIA, Frédéric Besson INRIA, Ninet Tristan Thales

Wed 17 Jan
Displayed time zone: London change

	08:50 - 09:00	Welcome from the ChairPOPL at Kelvin Lecture +0min

09:00 - 10:00	Keynote 1POPL at Kelvin Lecture Chair(s): Derek Dreyer MPI-SWS

09:00 60m Talk		A New Perspective on Commutativity in Verification POPL Azadeh Farzan University of Toronto

10:30 - 11:50	Synthesis 1POPL at Kelvin Lecture Chair(s): Soham Chakraborty TU Delft

10:30 20m Talk		Implementation and Synthesis of Math Library FunctionsDistinguished Paper POPL Ian Briggs University of Utah, Yash Lad University of Utah, Pavel Panchekha University of Utah
10:50 20m Talk		Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations POPL Yuantian Ding Purdue University, Xiaokang Qiu Purdue University
11:10 20m Talk		Efficient Bottom-Up Synthesis for Programs with Local Variables POPL Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan Pre-print
11:30 20m Talk		Optimal Program Synthesis via Abstract Interpretation POPL Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania

13:20 - 14:40	Effect HandlersPOPL at Kelvin Lecture Chair(s): Cătălin Hriţcu MPI-SP

13:20 20m Talk		Soundly Handling LinearityDistinguished Paper POPL Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, Sam Lindley University of Edinburgh, J. Garrett Morris University of Iowa DOI Pre-print
13:40 20m Talk		Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers POPL Fuga Kawamata Waseda University, Hiroshi Unno University of Tsukuba, Taro Sekiyama National Institute of Informatics, Tachio Terauchi Waseda University
14:00 20m Talk		Effectful Software Contracts POPL Cameron Moy Northeastern University, Christos Dimoulas Northwestern University, Matthias Felleisen Northeastern University
14:20 20m Talk		Algebraic Effects Meet Hoare Logic in Cubical Agda POPL Donnacha Oisín Kidney Imperial College London, Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London Pre-print

15:10 - 16:30	Automata And ComplexityPOPL at Kelvin Lecture Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital

15:10 20m Talk		Parikh's Theorem Made Symbolic POPL Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
15:30 20m Talk		Efficient Matching of Regular Expressions with Lookaround Assertions POPL Konstantinos Mamouras Rice University, Agnishom Chattopadhyay Rice University
15:50 20m Talk		The Complex(ity) Landscape of Checking Infinite Descent POPL Liron Cohen Ben-Gurion University of the Negev, Adham Jabarin Ben Gurion University, Andrei Popescu University of Sheffield, Reuben N. S. Rowe Royal Holloway University of London
16:10 20m Talk		Positive Almost-Sure Termination – Complexity and Proof Rules POPL Rupak Majumdar MPI-SWS, V.R. Sathiyanarayana MPI-SWS

16:50 - 18:10	ConcurrencyPOPL at Kelvin Lecture Chair(s): Sophia Drossopoulou Imperial College London

16:50 20m Talk		A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability POPL Prasad Jayanti Department of Computer Science, Dartmouth College, USA, Siddhartha Jayanti Google Research, Ugur Y. Yavuz Boston University, Lizzie Hernandez Videa Microsoft
17:10 20m Talk		Predictive Monitoring against Pattern Regular Languages POPL Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore Pre-print
17:30 20m Talk		Commutativity Simplifies Proofs of Parameterized Programs POPL Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg Pre-print
17:50 20m Talk		Coarser Equivalences for Causal Concurrency POPL Azadeh Farzan University of Toronto, Umang Mathur National University of Singapore Pre-print

Thu 18 Jan
Displayed time zone: London change

09:00 - 10:20	Synthesis 2POPL at Kelvin Lecture Chair(s): Michael Hicks Amazon Web Services and the University of Maryland

09:00 20m Talk		Semantic Code Refactoring for Abstract Data Types POPL Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
09:20 20m Talk		API-driven Program Synthesis for Testing Static Typing Implementations POPL Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich
09:40 20m Talk		Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs POPL Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
10:00 20m Talk		A Case for Synthesis of Recursive Quantum Unitary Programs POPL Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland

10:50 - 12:10	Types 2POPL at Kelvin Lecture Chair(s): Stefan K. Muller Illinois Institute of Technology

10:50 20m Talk		Quotient Haskell: Lightweight Quotient Types for All POPL Brandon Hewer University of Nottingham, Graham Hutton University of Nottingham, UK
11:10 20m Talk		Focusing on Refinement Typing (TOPLAS)Remote POPL Dimitrios Economou Queen's University, Canada, Neel Krishnaswami University of Cambridge, Jana Dunfield Queen's University, Kingston, Ontario Link to publication
11:30 20m Talk		Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote POPL Guannan Wei Purdue University, Oliver Bračevac Galois, Inc., Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
11:50 20m Talk		Capturing Types (TOPLAS) POPL Aleksander Boruch-Gruszecki EPFL, Martin Odersky EPFL, Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen DOI File Attached

13:40 - 15:00	Quantum ComputingPOPL at Kelvin Lecture Chair(s): Oded Padon VMware Research

13:40 20m Talk		With a Few Square Roots, Quantum Computing is as Easy as Pi POPL Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University Pre-print
14:00 20m Talk		Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers POPL Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy
14:20 20m Talk		SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationRemote POPL Yuxiang Peng University of Maryland, Jacob Young University of Maryland, Pengyu Liu Tsinghua University, Xiaodi Wu University of Maryland
14:40 20m Talk		Enriched Presheaf Model of Quantum FPC POPL Takeshi Tsukada Chiba University, Kazuyuki Asada Tohoku University

15:30 - 16:50	ParallelismPOPL at Kelvin Lecture Chair(s): John Reppy University of Chicago, USA

15:30 20m Talk		Pipelines and Beyond: Graph Types for ADTs with Futures POPL Francis Rinaldi Illinois Institute of Technology, june wunder Boston University, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Stefan K. Muller Illinois Institute of Technology
15:50 20m Talk		Disentanglement with Futures, State, and Interaction POPL Jatin Arora Carnegie Mellon University, Stefan K. Muller Illinois Institute of Technology, Umut A. Acar Carnegie Mellon University
16:10 20m Talk		DisLog: A Separation Logic for Disentanglement POPL Alexandre Moine Inria, Sam Westrick Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University Pre-print
16:30 20m Talk		Automatic Parallelism ManagementDistinguished Paper POPL Sam Westrick Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Mike Rainey Carnegie Mellon University, Umut A. Acar Carnegie Mellon University

17:10 - 18:20	SIGPLAN Awards, PC Chair's Report, and Business MeetingPOPL at Kelvin Lecture Chair(s): Philippa Gardner Imperial College London

17:10 70m Awards		SIGPLAN Awards, PC Chair's Report, and Business Meeting POPL

Fri 19 Jan
Displayed time zone: London change

08:50 - 09:00	WelcomePOPL at Kelvin Lecture +0min

08:50 10m Other		Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process POPL Alastair F. Donaldson Imperial College London, John Wickerson Imperial College London

09:00 - 10:00	Keynote 2POPL at Kelvin Lecture Chair(s): Alexandra Silva Cornell University

09:00 60m Talk		The Network is the Computer: A Programming Language Perspective POPL Nate Foster Cornell University and Jane Street

10:30 - 11:50	Program AnalysisPOPL at Kelvin Lecture Chair(s): Jules Villard Meta

10:30 20m Talk		Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis POPL John Cyphert University of Wisconsin-Madison, USA, Zachary Kincaid Princeton University
10:50 20m Talk		On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability POPL Shankaranarayanan Krishna IIT Bombay, India, Aniket Lal IIT Bombay, Andreas Pavlogiannis Aarhus University, Omkar Tuppe IIT Bombay
11:10 20m Talk		Monotonicity and the Precision of Program Analysis POPL Marco Campion INRIA & École Normale Supérieure \| Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria & École Normale Supérieure \| Université PSL
11:30 20m Talk		Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisDistinguished PaperRemote POPL Supun Abeysinghe Purdue University, Anxhelo Xhebraj Purdue University, Tiark Rompf Purdue University

13:20 - 14:40	Types 3POPL at Kelvin Lecture Chair(s): Steven Ramsay University of Bristol

13:20 20m Talk		When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism POPL Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), Aleksander Boruch-Gruszecki EPFL, Andong Fan HKUST (The Hong Kong University of Science and Technology), Chun Yin Chau HKUST (The Hong Kong University of Science and Technology) DOI Pre-print Media Attached File Attached
13:40 20m Talk		Parametric Subtyping for Structural Parametric PolymorphismDistinguished PaperRemote POPL Henry DeYoung CMU, Andreia Mordido University of Lisbon, Frank Pfenning Carnegie Mellon University, USA, Ankush Das Amazon
14:00 20m Talk		Unboxed data constructors -- or, how cpp decides a halting problem POPL Nicolas Chataing ENS Paris, Stephen Dolan Jane Street, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
14:20 20m Talk		Polymorphic Type Inference for Dynamic Languages POPL Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université Paris Cité / IRIF, Kim Nguyễn Université Paris-Saclay Link to publication DOI

15:10 - 16:30	Machine and Automata LearningPOPL at Kelvin Lecture Chair(s): Steven Holtzen Northeastern University

15:10 20m Talk		Efficient CHAD POPL Tom Smeding Utrecht University, Matthijs Vákár Utrecht University DOI Pre-print
15:30 20m Talk		ReLU Hull Approximation POPL Zhongkui Ma The University of Queensland, Jiaying LI Microsoft, Guangdong Bai The University of Queensland
15:50 20m Talk		On Learning Polynomial Recursive Programs POPL Alex Buna-Marginean University of Oxford, Vincent Cheval Inria Paris, Mahsa Shirmohammadi CNRS & IRIF, Paris, James Worrell University of Oxford
16:10 20m Talk		Programming-by-Demonstration for Long-Horizon Robot Tasks POPL Noah Patton The University of Texas at Austin, Kia Rahmani The University of Texas at Austin, Meghana Missula The University of Texas at Austin, Joydeep Biswas The University of Texas at Austin, Işıl Dillig University of Texas at Austin

16:50 - 18:10	Gradual Typing and VerificationPOPL at Kelvin Lecture Chair(s): Ronald Garcia University of British Columbia

16:50 20m Talk		Securing Verified IO Programs Against Unverified Code in F* POPL Cezar-Constantin Andrici MPI-SP, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology, Éric Tanter University of Chile, Théo Winterhalter INRIA Saclay Pre-print
17:10 20m Talk		Sound Gradual Verification with Symbolic Execution POPL Conrad Zimmerman Brown University, Jenna DiVincenzo (Wise) Purdue University, Jonathan Aldrich Carnegie Mellon University
17:30 20m Talk		Type-based Gradual Typing Performance Optimization POPL John Peter Campora Quantinuum, Mohammad Wahiduzzaman Khan UL Lafayette, Sheng Chen UL Lafayette
17:50 20m Talk		Total Type Error Localization and Recovery with HolesDistinguished Paper POPL Eric Zhao University of Michigan, Raef Maroof University of Michigan, Anand Dukkipati University of Michigan, Andrew Blinn University of Michigan, Zhiyi Pan University of Michigan, Cyrus Omar University of Michigan

	18:10 - 18:15	Farewell from the ChairPOPL at Kelvin Lecture +0min

Sat 20 Jan
Displayed time zone: London change

09:00 - 10:30	Session 1CoqPL at Kelvin Lecture

09:00 5m Day opening		Introduction CoqPL
09:05 60m Keynote		Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk) CoqPL I: Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria File Attached
10:05 25m Talk		CertiCoq-Wasm: Verified compilation from Coq to WebAssembly CoqPL Wolfgang Meier , Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University File Attached

11:00 - 12:30	Session 2CoqPL at Kelvin Lecture

11:00 90m Panel		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria, Yves Bertot INRIA, Emilio Jesús Gallego Arias INRIA

14:00 - 15:30	Session 3CoqPL at Kelvin Lecture

14:00 22m Talk		Well-founded recursion done right CoqPL Xavier Leroy Collège de France File Attached
14:22 22m Talk		Functorial Syntax for All CoqPL Filip Sieczkowski Heriot-Watt University, Piotr Polesiuk University of Wrocław File Attached
14:45 22m Talk		Specifying Smart Contract with Hax and ConCert CoqPL Lasse Letager Hansen Aarhus University, Bas Spitters Aarhus University File Attached
15:07 22m Talk		A formal security analysis of Blockchain voting CoqPL Nikolaj Sidorenco Aarhus University, Laura Brædder , Lasse Letager Hansen Aarhus University, Eske Hoy Nielsen Aarhus University, Bas Spitters Aarhus University File Attached

16:00 - 17:30	Session 4CoqPL at Kelvin Lecture

16:00 22m Talk		InducTeX: A MetaCoq plugin for typesetting inductive definitions CoqPL Jacco Krijnen Utrecht University File Attached
16:22 22m Talk		VsCoq 2, new foundations CoqPL Romain Tetley File Attached
16:45 22m Talk		Integrating Dependency Building with Document Checking in Coq CoqPL Emilio Jesús Gallego Arias INRIA, Bhakti Shah University of Chicago File Attached
17:07 22m Talk		A diagram editor to mechanize categorical proofs CoqPL Ambroise Lafont Ecole Polytechnique File Attached

Sun 14 Jan
Displayed time zone: London 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
Kelvin Lecture	LAFI First Session																								LAFI Second Session																																				LAFI Third Session																								LAFI Poster and Interactive Session

Mon 15 Jan
Displayed time zone: London 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						18:00						30
Kelvin Lecture	CPP Logic and Beyond																								CPP Compiler / Program Verification																																				CPP Isabelle, PVS																								CPP Formalizing Mathematics																			CPP Business Meeting

Tue 16 Jan
Displayed time zone: London 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
Kelvin Lecture	CPP Interactive Proof Development																								CPP Formalizations of Category Theory																																				CPP Mechanized separation logic																								CPP Verified Compilation

Wed 17 Jan
Displayed time zone: London 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
Kelvin Lecture											POPL Welcome from the Chair		POPL Keynote 1																		POPL Synthesis 1																																		POPL Effect Handlers																						POPL Automata And Complexity																				POPL Concurrency

Thu 18 Jan
Displayed time zone: London 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						18:00						30
Kelvin Lecture	POPL Synthesis 2																						POPL Types 2																																		POPL Quantum Computing																						POPL Parallelism																				POPL SIGPLAN Awards, PC Chair's Report, and Business Meeting

Fri 19 Jan
Displayed time zone: London 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
Kelvin Lecture											POPL Welcome		POPL Keynote 2																		POPL Program Analysis																																		POPL Types 3																						POPL Machine and Automata Learning																				POPL Gradual Typing and Verification																POPL Farewell from the Chair

Sat 20 Jan
Displayed time zone: London 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
Kelvin Lecture	CoqPL Session 1																								CoqPL Session 2																																				CoqPL Session 3																								CoqPL Session 4

Sun 14 Jan
Displayed time zone: London 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
Kelvin Lecture	LAFI Opening Remarks 09:00 - 09:10		LAFI Hong Ge: Bayesian inference using probabilistic programming 09:10 - 10:10												LAFI Basis Talk 10:10 - 10:30										LAFI A Tree Sampler for Bounded Context-Free Languages 11:00 - 11:10		LAFI A Multi-language Approach to Probabilistic Program Inference 11:10 - 11:20		LAFI Belief Programming in Partially Observable Probabilistic Environments 11:20 - 11:30		LAFIOnline Homomorphic Reverse Differentiation of Iteration 11:30 - 11:40		LAFI MultiSPPL: extending SPPL with multivariate leaf nodes 11:40 - 11:50		LAFI Reverse mode ADEV via YOLO: tangent estimators transpose to gradient es ... 11:50 - 12:00		LAFI Sparse Differentiation in Computer Graphics 12:00 - 12:10		LAFI A slice sampler for the Indian Buffet Process: expressivity in nonparam ... 12:10 - 12:20		LAFI Effective Sequential Monte Carlo for Language Model Probabilistic Programs 12:20 - 12:30																				LAFI Effect Handlers for Choice-Based Learning 14:00 - 14:10		LAFI Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Ge ... 14:10 - 14:20		LAFI JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS ... 14:20 - 14:30		LAFI Mixture Languages 14:30 - 14:40		LAFI Structured Tensor Algebra for Efficient Discrete Probabilistic Inference 14:40 - 14:50		LAFI Towards a Categorical Model of the Lilac Separation Logic 14:50 - 15:00		LAFI Toward Probabilistic Coarse-to-Fine Program Synthesis 15:00 - 15:10		LAFIOnline Static Posterior Inference of Bayesian Probabilistic Programming via Po ... 15:10 - 15:20		LAFIOnline Abstract Interpretation for Automatic Differentiation 15:20 - 15:30

Mon 15 Jan
Displayed time zone: London 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
Kelvin Lecture	CPP Under-approximation for Scalable Bug Detection 09:00 - 10:00												CPP A mechanised and constructive reverse analysis of soundness and complet ... 10:00 - 10:30												CPP The Last Yard: Foundational End-to-End Verification of High-Speed Crypt ... 11:00 - 11:30						CPP UTC time, formally verified 11:30 - 12:00						CPP VCFloat2: Floating-point error analysis in Coq 12:00 - 12:30																								CPPremote presentation A Temporal Differential Dynamic Logic Formal Embedding 14:00 - 14:30						CPPdistinguished paper Formal Probabilistic Methods for Combinatorial Structures using the Lov ... 14:30 - 15:00						CPP Certification of Confluence- and Commutation-Proofs via Parallel Critic ... 15:00 - 15:30												CPP A Formalization of Complete Discrete Valuation Rings and Local Fields 16:00 - 16:30						CPP Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture 16:30 - 17:00						CPPremote presentation Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multipl ... 17:00 - 17:30							CPP Business Meeting 17:35 - 18:30

Tue 16 Jan
Displayed time zone: London 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
Kelvin Lecture	CPP Improved Assistance for Interactive Proof 09:00 - 10:00												CPPdistinguished paper Martin-Löf à la Coq 10:00 - 10:30												CPP Displayed Monoidal Categories for the Semantics of Linear Logic 11:00 - 11:30						CPP Univalent Double Categories 11:30 - 12:00						CPP Formalizing the ∞-categorical Yoneda lemma 12:00 - 12:30																								CPP Compositional Verification of Concurrent C Programs with Search Structu ... 14:00 - 14:30						CPPdistinguished paper Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in ... 14:30 - 15:00						CPP Unification for Subformula Linking under Quantifiers 15:00 - 15:30												CPP Lean Formalization of Extended Regular Expression Matching with Lookarounds 16:00 - 16:30						CPP Memory simulations, security and optimization in a verified compiler 16:30 - 17:00						CPP PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Deci ... 17:00 - 17:30

Wed 17 Jan
Displayed time zone: London 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
Kelvin Lecture	POPL A New Perspective on Commutativity in Verification 09:00 - 10:00																		POPL Distinguished Paper Implementation and Synthesis of Math Library Functions 10:30 - 10:50				POPL Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vect ... 10:50 - 11:10				POPL Efficient Bottom-Up Synthesis for Programs with Local Variables 11:10 - 11:30				POPL Optimal Program Synthesis via Abstract Interpretation 11:30 - 11:50																						POPL Distinguished Paper Soundly Handling Linearity 13:20 - 13:40				POPL Answer Refinement Modification: Refinement Type System for Algebraic Ef ... 13:40 - 14:00				POPL Effectful Software Contracts 14:00 - 14:20				POPL Algebraic Effects Meet Hoare Logic in Cubical Agda 14:20 - 14:40										POPL Parikh's Theorem Made Symbolic 15:10 - 15:30				POPL Efficient Matching of Regular Expressions with Lookaround Assertions 15:30 - 15:50				POPL The Complex(ity) Landscape of Checking Infinite Descent 15:50 - 16:10				POPL Positive Almost-Sure Termination – Complexity and Proof Rules 16:10 - 16:30								POPL A Universal, Sound, and Complete Forward Reasoning Technique for Machin ... 16:50 - 17:10				POPL Predictive Monitoring against Pattern Regular Languages 17:10 - 17:30				POPL Commutativity Simplifies Proofs of Parameterized Programs 17:30 - 17:50				POPL Coarser Equivalences for Causal Concurrency 17:50 - 18:10

Thu 18 Jan
Displayed time zone: London 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
Kelvin Lecture	POPL Semantic Code Refactoring for Abstract Data Types 09:00 - 09:20				POPL API-driven Program Synthesis for Testing Static Typing Implementations 09:20 - 09:40				POPL Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilis ... 09:40 - 10:00				POPL A Case for Synthesis of Recursive Quantum Unitary Programs 10:00 - 10:20										POPL Quotient Haskell: Lightweight Quotient Types for All 10:50 - 11:10				POPL Remote Focusing on Refinement Typing (TOPLAS) 11:10 - 11:30				POPL Remote Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separ ... 11:30 - 11:50				POPL Capturing Types (TOPLAS) 11:50 - 12:10																						POPL With a Few Square Roots, Quantum Computing is as Easy as Pi 13:40 - 14:00				POPL Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-D ... 14:00 - 14:20				POPL Remote SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with ... 14:20 - 14:40				POPL Enriched Presheaf Model of Quantum FPC 14:40 - 15:00										POPL Pipelines and Beyond: Graph Types for ADTs with Futures 15:30 - 15:50				POPL Disentanglement with Futures, State, and Interaction 15:50 - 16:10				POPL DisLog: A Separation Logic for Disentanglement 16:10 - 16:30				POPL Distinguished Paper Automatic Parallelism Management 16:30 - 16:50								POPL SIGPLAN Awards, PC Chair's Report, and Business Meeting 17:10 - 18:20

Fri 19 Jan
Displayed time zone: London 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
Kelvin Lecture											POPL Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review ... 08:50 - 09:00		POPL The Network is the Computer: A Programming Language Perspective 09:00 - 10:00																		POPL Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis 10:30 - 10:50				POPL On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability 10:50 - 11:10				POPL Monotonicity and the Precision of Program Analysis 11:10 - 11:30				POPL Distinguished PaperRemote Flan: An Expressive and Efficient Datalog Compiler for Program Analysis 11:30 - 11:50																						POPL When Subtyping Constraints Liberate: A Novel Type Inference Approach fo ... 13:20 - 13:40				POPL Distinguished PaperRemote Parametric Subtyping for Structural Parametric Polymorphism 13:40 - 14:00				POPL Unboxed data constructors -- or, how cpp decides a halting problem 14:00 - 14:20				POPL Polymorphic Type Inference for Dynamic Languages 14:20 - 14:40										POPL Efficient CHAD 15:10 - 15:30				POPL ReLU Hull Approximation 15:30 - 15:50				POPL On Learning Polynomial Recursive Programs 15:50 - 16:10				POPL Programming-by-Demonstration for Long-Horizon Robot Tasks 16:10 - 16:30								POPL Securing Verified IO Programs Against Unverified Code in F* 16:50 - 17:10				POPL Sound Gradual Verification with Symbolic Execution 17:10 - 17:30				POPL Type-based Gradual Typing Performance Optimization 17:30 - 17:50				POPL Distinguished Paper Total Type Error Localization and Recovery with Holes 17:50 - 18:10

Sat 20 Jan
Displayed time zone: London 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
Kelvin Lecture	CoqPL Introduction 09:00 - 09:05	CoqPL Melocoton: A Program Logic for Verified Interoperability Between OCaml ... 09:05 - 10:05												CoqPL CertiCoq-Wasm: Verified compilation from Coq to WebAssembly 10:05 - 10:30											CoqPL Session with the Coq Development Team 11:00 - 12:30																																				CoqPL Well-founded recursion done right 14:00 - 14:22				CoqPL Functorial Syntax for All 14:22 - 14:45					CoqPL Specifying Smart Contract with Hax and ConCert 14:45 - 15:07				CoqPL A formal security analysis of Blockchain voting 15:07 - 15:30											CoqPL InducTeX: A MetaCoq plugin for typesetting inductive definitions 16:00 - 16:22				CoqPL VsCoq 2, new foundations 16:22 - 16:45					CoqPL Integrating Dependency Building with Document Checking in Coq 16:45 - 17:07				CoqPL A diagram editor to mechanize categorical proofs 17:07 - 17:30

Room information: Kelvin Lecture

Program Display Configuration

Sun 14 JanDisplayed time zone: London change

Mon 15 JanDisplayed time zone: London change

Tue 16 JanDisplayed time zone: London change

Wed 17 JanDisplayed time zone: London change

Thu 18 JanDisplayed time zone: London change

Fri 19 JanDisplayed time zone: London change

Sat 20 JanDisplayed time zone: London change

Sun 14 JanDisplayed time zone: London change

LAFI

LAFI

LAFI

LAFI

Mon 15 JanDisplayed time zone: London change

CPP

CPP

CPP

CPP

CPP

Tue 16 JanDisplayed time zone: London change

CPP

CPP

CPP

CPP

Wed 17 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

POPL

POPL

Thu 18 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

POPL

Fri 19 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

POPL

POPL

POPL

Sat 20 JanDisplayed time zone: London change

CoqPL

CoqPL

CoqPL

CoqPL

Sun 14 JanDisplayed time zone: London change

Mon 15 JanDisplayed time zone: London change

Tue 16 JanDisplayed time zone: London change

Wed 17 JanDisplayed time zone: London change

Thu 18 JanDisplayed time zone: London change

Fri 19 JanDisplayed time zone: London change

Sat 20 JanDisplayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change