POPL 2024
Sun 14 - Sat 20 January 2024
London, United Kingdom
Toggle navigation
Attending
Venue: Institution of Engineering and Technology
Supporting POPL
Registration
Conference Hotel: Strand Palace Hotel
Information for Virtual Attendees
Information for Presenters
Requesting a Visa
POPL Live Streams
Program
POPL Program
Your Program
Filter by Day
Sun 14 Jan
Mon 15 Jan
Tue 16 Jan
Wed 17 Jan
Thu 18 Jan
Fri 19 Jan
Sat 20 Jan
Tracks
POPL 2024
Artifact Evaluation
Diversity, Equity and Inclusion
POPL
Session Previews
Student Research Competition
Student Volunteers
TutorialFest
Workshops and Co-located Events
Co-hosted Conferences
CPP
VMCAI
Workshops
CoqPL
Dafny
GALOP
Incorrectness
LAFI
N40AI
O'Hearn Fest
PEPM
PLMW @ POPL
PLanQC
POCL
PROPL
PriSC
The Future of Weak Memory
WAW
WITS
Co-hosted Symposia
PADL
Organization
POPL 2024 Committees
Organizing Committee
AV Committee
Student Volunteers
Track Committees
Artifact Evaluation
Diversity, Equity and Inclusion
POPL
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CPP
Organizing Committee
Program Committee
Steering Committee
VMCAI
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Program Committee
Dafny
Program Chairs
Program Committee
Steering Committee
GALOP
Invited Speakers
Organising Committee
Program Committee
Incorrectness
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
N40AI
Organizing Committee
O'Hearn Fest
Program Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PLanQC
Organizing Committee
Program Committee
POCL
Organizing Committee
Program Committee
PROPL
Chairs
Programme Committee
PriSC
Program Committee
Steering Committee
The Future of Weak Memory
Organizing Committee
Program Committee
WAW
Organizing Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Program Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2024
(
series
) /
Institution of Engineering and Technology
/
Room information: Kelvin Lecture
Venue
Institution of Engineering and Technology
Room name
Kelvin Lecture
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT) London
.
Use conference time zone: (GMT) London
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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 Session
LAFI
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 Session
LAFI
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 Iteration
Online
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 Session
LAFI
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 Solving
Online
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 Differentiation
Online
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 Session
LAFI
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 Beyond
CPP
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 Verification
CPP
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, PVS
CPP
at
Kelvin Lecture
Chair(s):
Dmitriy Traytel
University of Copenhagen
14:00
30m
Talk
A Temporal Differential Dynamic Logic Formal Embedding
remote 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 Lemma
distinguished 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 Mathematics
CPP
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 Arguments
remote presentation
CPP
Joseph Eremondi
University of Regina
Pre-print
17:35 - 18:30
Business Meeting
CPP
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 Coq
distinguished 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 Theory
CPP
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 logic
CPP
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 Logic
distinguished 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 Compilation
CPP
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 Chair
POPL
at
Kelvin Lecture
+0min
09:00 - 10:00
Keynote 1
POPL
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 1
POPL
at
Kelvin Lecture
Chair(s):
Soham Chakraborty
TU Delft
10:30
20m
Talk
Implementation and Synthesis of Math Library Functions
Distinguished 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 Handlers
POPL
at
Kelvin Lecture
Chair(s):
Cătălin Hriţcu
MPI-SP
13:20
20m
Talk
Soundly Handling Linearity
Distinguished 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 Complexity
POPL
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
Concurrency
POPL
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 2
POPL
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 2
POPL
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 Programs
Remote
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 Computing
POPL
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 Compilation
Remote
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
Parallelism
POPL
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 Management
Distinguished 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 Meeting
POPL
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
Welcome
POPL
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 2
POPL
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 Analysis
POPL
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 Analysis
Distinguished Paper
Remote
POPL
Supun Abeysinghe
Purdue University
,
Anxhelo Xhebraj
Purdue University
,
Tiark Rompf
Purdue University
13:20 - 14:40
Types 3
POPL
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 Polymorphism
Distinguished Paper
Remote
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 Learning
POPL
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 Verification
POPL
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 Holes
Distinguished 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 Chair
POPL
at
Kelvin Lecture
+0min
Sat 20 Jan
Displayed time zone:
London
change
09:00 - 10:30
Session 1
CoqPL
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 2
CoqPL
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 3
CoqPL
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 4
CoqPL
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
LAFI
Online
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
LAFI
Online
Static Posterior Inference of Bayesian Probabilistic Programming via Po ...
15:10 - 15:20
LAFI
Online
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
CPP
remote presentation
A Temporal Differential Dynamic Logic Formal Embedding
14:00 - 14:30
CPP
distinguished 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
CPP
remote 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
CPP
distinguished 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
CPP
distinguished 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 Paper
Remote
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 Paper
Remote
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
x
Sat 7 Dec 02:58