POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
VenueInstitution of Engineering and Technology
Room nameKelvin Lecture
Room InformationNo extra information available
Program

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

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 Gonzá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

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
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
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

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Kelvin Lecture

Sun 14 Jan

Displayed time zone: London change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
Kelvin Lecture
LAFI
Opening Remarks
09:00 - 09:10
LAFI
Basis Talk
10:10 - 10:30

Fri 19 Jan

Displayed time zone: London change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
Kelvin Lecture
POPL
Efficient CHAD
15:10 - 15:30