POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
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
Morning Track 1TutorialFest at Haslett Room
09:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote
TutorialFest
P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign
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

09:00 - 10:30
Session 1GALOP at Lovelace Room
Chair(s): Pierre Clairambault CNRS & LIS, Aix-Marseille Université
09:00
45m
Keynote
On Interaction, Efficiency, and Reversibility
GALOP
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis
09:45
22m
Talk
Normal Form Bisimulations by Value
GALOP
Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Claudia Faggian Université de Paris & CNRS
10:08
22m
Talk
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
GALOP
Nikos Tzevelekos Queen Mary University of London, Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Queen Mary University of London
09:00 - 10:30
Morning Track 2TutorialFest at Marconi Room
09:00
90m
Talk
MetaCoq Tutorial
TutorialFest
Yannick Forster Inria, Meven Lennon-Bertrand University of Cambridge, Matthieu Sozeau Inria, Theo Winterhalter INRIA Saclay
09:00 - 10:30
Session 1O'Hearn Fest at Mountbatten Exhibition
Chair(s): Matthew J. Parkinson Microsoft Azure Research
09:00
22m
Talk
Introduction
O'Hearn Fest
Azalea Raad Imperial College London, Jules Villard Meta
09:22
22m
Talk
Peter's early work on parametricity, and why it still matters to me
O'Hearn Fest
Hongseok Yang KAIST; IBS
09:45
22m
Talk
Strong vs. weak separating conjunction in CSL
O'Hearn Fest
10:07
22m
Talk
Verified Software at Scale
O'Hearn Fest
Philippa Gardner Imperial College London
09:00 - 10:30
ApplicationsDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche Amazon Web Services, Joseph Tassarotti NYU
09:10
60m
Keynote
Verifying a concurrent file system with sequential reasoning
Dafny
Tej Chajed UW-Madison
10:12
18m
Talk
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Dafny
Alessandro Cimatti Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Gianluca Redondi Fondazione Bruno Kessler
10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Morning Track 1TutorialFest at Haslett Room
11:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote
TutorialFest
P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign
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
11:00 - 12:30
Session 2GALOP at Lovelace Room
Chair(s): Nikos Tzevelekos Queen Mary University of London
11:00
22m
Talk
Operational game semantics for generative algebraic effects and handlers
GALOP
Hamza Jaâfar Inria, Guilhem Jaber Nantes Université
11:23
22m
Talk
An abstract, certified account of Operational Game Semantics
GALOP
Peio Borthelle Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, LAMA, 73000 Chambéry, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Guilhem Jaber Nantes Université, Yannick Zakowski Inria
11:45
22m
Talk
Operational Algorithmic Game Semantics
GALOP
Benedict Bunting University of Oxford, Andrzej Murawski University of Oxford
12:08
22m
Talk
An algebraic theory of named threads (work in progress)
GALOP
Cristina Matache University of Edinburgh
11:00 - 12:30
Morning Track 2TutorialFest at Marconi Room
11:00
90m
Talk
MetaCoq Tutorial
TutorialFest
Yannick Forster Inria, Meven Lennon-Bertrand University of Cambridge, Matthieu Sozeau Inria, Theo Winterhalter INRIA Saclay
11:00 - 12:30
Testing and Teaching / ComparisonDafny at Turing Lecture
Chair(s): Joseph Tassarotti NYU
11:00
18m
Talk
Dafny Test Generationremote
Dafny
Aleksandr Fedchin Tufts University, Jeffrey S. Foster Tufts University, Zvonimir Rakamaric Amazon Web Services, Aaron Tomb Amazon Web Services
11:18
18m
Talk
Randomised Testing of the Dafny Compiler
Dafny
Alastair F. Donaldson Imperial College London, Dilan Sheth Imperial College London, Jean-Baptiste Tristan Amazon Web Services, Alex Usher Imperial College London
11:36
18m
Talk
Teaching Logic and Set Theory with Dafny
Dafny
Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan, Hezi Daniel Israel Academic College in Ramat Gan
11:54
18m
Talk
Learn 'em Dafny
Dafny
James Noble Creative Research & Programming
Pre-print
12:12
18m
Talk
Colouring Flags with Dafny & Idris
Dafny
Jan de Muijnck-Hughes University of Strathclyde, James Noble Creative Research & Programming
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Afternoon Track 1TutorialFest at Haslett Room
14:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
TutorialFest
Constantin Enea Ecole Polytechnique / LIX / CNRS, Shaz Qadeer Facebook
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
14:00 - 15:30
Session 3GALOP at Lovelace Room
Chair(s): Hugo Paquet LIPN, Université Sorbonne Paris Nord
14:00
45m
Keynote
Compositional Development of Certified System Software
GALOP
Zhong Shao Yale University
14:45
22m
Talk
SSA is Freyd Categories
GALOP
Jad Elkhaleq Ghalayini University of Cambridge
15:08
22m
Talk
A Denotational Approach to Release/Acquire Concurrency
GALOP
Yotam Dvir Tel Aviv University, Ohad Kammar University of Edinburgh, Ori Lahav Tel Aviv University
14:00 - 15:30
Afternoon Track 2TutorialFest at Marconi Room
14:00
90m
Tutorial
String Solving for Verification
TutorialFest
Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer University of Regensburg and Uppsala University
14:00 - 15:30
14:00
22m
Talk
Massive proofs for the masses
O'Hearn Fest
Byron Cook Amazon
14:22
22m
Talk
Designing Wait-free Weak Reference Counting
O'Hearn Fest
Matthew J. Parkinson Microsoft Azure Research
14:45
22m
Talk
Elegance and generosity are scientific values - And other things I've learned from Peter
O'Hearn Fest
Jade Alglave Arm and University College London
15:07
22m
Talk
Peter, the May and the Must, and Lacework
O'Hearn Fest
14:00 - 15:30
Proof Stability / Brittleness / ScaleDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
14:00
18m
Talk
Enhancing Proof Stability
Dafny
Sean McLaughlin Amazon Web Services, Georges-Axel Jaloyan Amazon Web Services, Tongtong Xiang Amazon Web Services, Florian Rabe Amazon Web Services
14:18
18m
Talk
Improving the Stability of Type Safety Proofs in Dafny
Dafny
Joseph W. Cutler University of Pennsylvania, Michael Hicks Amazon Web Services and the University of Maryland, Emina Torlak Amazon Web Services, USA
14:36
18m
Talk
Incremental Proof Development in Dafny with Module-Based Induction
Dafny
14:54
18m
Talk
Portfolio Solving for Dafny
Dafny
Eric Mugnier University of California San Diego, Sean McLaughlin Amazon Web Services, Aaron Tomb Amazon Web Services
15:12
18m
Talk
Domesticating Automation
Dafny
Pranav Srinivasan University of Michigan / VMware Research, Oded Padon VMware Research, Jon Howell VMware Research, Andrea Lattuada VMware Research
15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Afternoon Track 1TutorialFest at Haslett Room
16:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
TutorialFest
Constantin Enea Ecole Polytechnique / LIX / CNRS, Shaz Qadeer Facebook
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.

16:00 - 17:52
Session 4GALOP at Lovelace Room
Chair(s): Guilhem Jaber Nantes Université
16:00
22m
Talk
Invisible pebbles and the geometry of affine higher-order tree transducers
GALOP
Lê Thành Dũng Nguyễn École normale supérieure de Lyon, Gabriele Vanoni IRIF, Université Paris Cité
16:22
22m
Talk
Taylor Expansion is Game Semantics
GALOP
Lison Blondeau-Patissier LIS & I2M, Aix-Marseille Université, Pierre Clairambault CNRS & LIS, Aix-Marseille Université, Lionel Vaux Auclair University of Aix-Marseille
16:44
22m
Talk
Game-enriched categories
GALOP
Paul Blain Levy University of Birmingham
17:07
22m
Talk
Fair omega-Regular Games
GALOP
Daniel Hausmann University of Gothenburg, Nir Piterman University Gothenburg, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Anne-Kathrin Schmuck Max Planck Institute for Software Systems
17:29
22m
Talk
MELL proof-nets without boxes: thirty years later
GALOP
Abhishek De University of Birmingham, Kostia Chardonnet Università di Bologna
16:00 - 17:30
Afternoon Track 2TutorialFest at Marconi Room
16:00
90m
Tutorial
String Solving for Verification
TutorialFest
Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer University of Regensburg and Uppsala University
16:00 - 17:30
16:00
22m
Talk
Working with Peter O'Hearn in academia and industry
O'Hearn Fest
Mark Harman Meta Platforms, Inc. and UCL
16:22
22m
Talk
Pete's Footprints
O'Hearn Fest
16:45
22m
Talk
Symbolic Execution with Separating Decision Diagrams
O'Hearn Fest
Josh Berdine SkipLabs
17:07
22m
Talk
With Peter from Theory to Engineering
O'Hearn Fest
16:00 - 17:30
Probabilistic Programs and Testing / Verifying ContractsDafny at Turing Lecture
Chair(s): Joseph Tassarotti NYU
16:00
18m
Talk
VMC: a Dafny Library for Verified Monte Carlo Algorithms
Dafny
Fabian Zaiser University of Oxford, Stefan Zetzsche Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services
16:18
18m
Talk
Caesar: A Verifier for Probabilistic Programs
Dafny
Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
16:36
18m
Talk
Verifying Dafny Contract Integrity
Dafny
Cassidy Waldrip Brigham Young University, Eric Mercer Brigham Young University
16:54
18m
Talk
Testing Specifications In Dafny
Dafny
Eli Goldweber University Of Michigan, Weixin Yu University Of Michigan, Armin Vakil University Of Michigan, Manos Kapritsos University of Michigan, USA
17:30 - 18:15
Code GenerationDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
17:30
18m
Talk
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Dafny
Christopher Brix RWTH Aachen University, Jean-Baptiste Tristan Amazon Web Services
17:48
18m
Talk
CLOVER: Closed-Loop Verifiable Code Generation
Dafny
Chuyue Sun Stanford University, Ying Sheng Stanford University, Oded Padon VMware Research, Clark Barrett Stanford University
18:06
9m
Day closing
Day closing
Dafny
Stefan Zetzsche Amazon Web Services, Joseph Tassarotti NYU

Mon 15 Jan

Displayed time zone: London change

09:00 - 10:30
Morning Track 3TutorialFest at Flowers Room
09:00
90m
Tutorial
Foundations of Type-Driven Probabilistic Modelling
TutorialFest
Ohad Kammar University of Edinburgh
Pre-print
09:00 - 10:30
Morning Track 1TutorialFest at Haslett Room
09:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
TutorialFest
Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL
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
09:00 - 10:30
Types and EffectsPADL at Lovelace Room
Chair(s): Martin Gebser University of Klagenfurt, Austria
09:00
60m
Keynote
Modular Higher-Order Effects
PADL
K: Nicolas Wu Imperial College London
10:00
30m
Talk
Asynchronous Reactive Programming with Modal Types in Haskell
PADL
Patrick Bahr IT University of Copenhagen, Emil Houlborg IT University of Copenhagen, Gregers Thomas Skat Rørdam IT University of Copenhagen
Pre-print
09:00 - 10:30
Session 1: Openning, Keynote, SAT, SMT and Automated ReasoningVMCAI at Marconi Room
Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security
09:00
5m
Day opening
Opening
VMCAI

09:05
60m
Keynote
Two Projects on Human Interaction with AI
VMCAI
David Harel Weizmann Institute of Science, Israel
10:05
20m
Talk
Interpolation and Quantifiers in Ortholattices
VMCAI
Sankalp Gambhir Ecole Polytechnique Federale de Lausanne (EPFL), Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland
09:00 - 10:30
09:00
90m
Tutorial
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
TutorialFest
Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
09:00 - 10:30
Session 1The Future of Weak Memory at Turing Lecture
Chair(s): John Wickerson Imperial College London
09:00
10m
Talk
Welcome
The Future of Weak Memory
John Wickerson Imperial College London, Azalea Raad Imperial College London, Brijesh Dongol University of Surrey, Mark Batty University of Kent, Peter Sewell University of Cambridge
09:10
20m
Talk
Some things I wish I hadn’t seen
The Future of Weak Memory
Matthew J. Parkinson Microsoft Azure Research
09:30
20m
Talk
Heterogeneous concurrency -- a new frontier for weak memory
The Future of Weak Memory
09:50
20m
Talk
Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Models
The Future of Weak Memory
Vasileios Klimis Queen Mary University of London
File Attached
10:10
20m
Talk
How Do We Know That Weak Memory Matters?
The Future of Weak Memory
Mike Dodds Galois, Inc.
File Attached
10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Morning Track 3TutorialFest at Flowers Room
11:00
90m
Tutorial
Foundations of Type-Driven Probabilistic Modelling
TutorialFest
Ohad Kammar University of Edinburgh
Pre-print
11:00 - 12:30
Morning Track 1TutorialFest at Haslett Room
11:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
TutorialFest
Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL
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, Theo 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
11:00 - 12:30
Knowledge Representation and LearningPADL at Lovelace Room
Chair(s): Jessica Zangari Università della Calabria
11:00
30m
Talk
Explanation and Knowledge Acquisition in Ad Hoc Teamwork
PADL
Hasra Dodampegama University of Birmingham, Mohan Sridharan University of Birmingham
11:30
30m
Talk
Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures
PADL
Teodoro Baldazzi Università degli Studi Roma Tre, Luigi Bellomarini Banca d'Italia, Marco Favorito Banca d'Italia, Emanuel Sallinger TU Wien & University of Oxford
12:00
30m
Talk
FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability
PADL
Huaduo Wang THE UNIVERSITY OF TEXAS AT DALLAS, Gopal Gupta University of Texas at Dallas
11:00 - 12:30
Session 2: SAT, SMT and Automated ReasoningVMCAI at Marconi Room
Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
11:00
20m
Talk
Function synthesis for maximizing model counting
VMCAI
Thomas Vigouroux VERIMAG - UGA, Marius Bozga CNRS; Université Grenoble Alpes, Cristian Ene Verimag, Grenoble, Laurent Mounier Université Grenoble Alpes
Pre-print
11:20
20m
Talk
Boosting Constrained Horn Solving by Unsat Core Learning
VMCAI
Parosh Aziz Abdulla Uppsala University, Sweden, Chencheng Liang Uppsala University, Philipp Rümmer University of Regensburg and Uppsala University
11:40
20m
Talk
On the Verification of a Subgraph Construction Algorithm
VMCAI
Lucas Böltz Univerity of Koblenz, Viorica Sofronie-Stokkermans University of Koblenz, Hannes Frey University of Koblenz
12:00
20m
Talk
Efficient Local Search for Nonlinear Real Arithmetic
VMCAI
Zhonghan Wang Institute of Software/CAS China, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Bohan Li State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, China, Shaowei Cai Institute of Software at Chinese Academy of Sciences
11:00 - 12:30
11:00
90m
Tutorial
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
TutorialFest
Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
11:00 - 12:30
Session 2The Future of Weak Memory at Turing Lecture
Chair(s): John Wickerson Imperial College London
11:00
22m
Talk
Weak Memory Demands Model-based Compiler Testing
The Future of Weak Memory
Luke Geeson University College London (UCL)
File Attached
11:22
22m
Talk
On the need for available, functional, and reusable memory models
The Future of Weak Memory
Hernán Ponce de León Huawei Dresden Research Center
11:45
22m
Talk
What we learned from C++ atomics and memory model standardization
The Future of Weak Memory
12:07
22m
Talk
Why Languages Should Preserve Load-Store Order
The Future of Weak Memory
Stephen Dolan Jane Street
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Afternoon Track 3TutorialFest at Flowers Room
14:00
90m
Tutorial
Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types
TutorialFest
Jonas Kastberg Hinrichsen Aarhus University, Denmark, Jules Jacobs Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
File Attached
14:00 - 15:30
Afternoon Track 1TutorialFest at Haslett Room
14:00
90m
Tutorial
Machine Learning Meets Program Synthesis
TutorialFest
Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute
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
14:00 - 15:30
Answer Set Programming IPADL at Lovelace Room
Chair(s): Gopal Gupta University of Texas at Dallas
14:00
30m
Talk
Marketplace Logistic via Answer Set Programming
PADL
Mario Alviano University of Calabria, Danilo Amendola Oliveru - Smartly Engineering, Luis Angel Rodriguez Reiners University of Calabria
14:30
30m
Talk
Rethinking Answer Set Programming Templates
PADL
Mario Alviano University of Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Jessica Zangari Università della Calabria
15:00
30m
Talk
A direct ASP encoding for Declare
PADL
Francesco Chiariello University of Naples Federico II, Valeria Fionda University of Calabria, Antonio Ielo University of Calabria, Francesco Ricca University of Calabria, Italy
14:00 - 15:30
Session 3: Security and Privacy, Model Checking and SynthesisVMCAI at Marconi Room
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
14:00
20m
Talk
Automatic and Incremental Repair for Speculative Information Leaks
VMCAI
Joachim Bard CISPA Helmholtz Center for Information Security, Swen Jacobs CISPA, Yakir Vizel Technion—Israel Institute of Technology
14:20
20m
Talk
Sound Abstract Nonexploitability Analysis
VMCAI
Francesco Parolini Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print
14:40
20m
Talk
Solving Two-Player Games under Progress Assumptions
VMCAI
Anne-Kathrin Schmuck MPI-SWS, K. S. Thejaswini The University of Warwick, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS)
Pre-print
15:00
20m
Talk
Model-Guided Synthesis for LTL over Finite Traces
VMCAI
Shengping Xiao East China Normal University, Yongkang Li East China Normal University, Xinyue Huang East China Normal University, Yicong Xu East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University, Ofer Strichman Technion, Moshe Vardi Rice University
15:20
10m
Talk
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
VMCAI
Daniel Hausmann University of Gothenburg, Merlin Humml Friedrich-Alexander Universität Erlangen-Nürnberg, Simon Prucker Friedrich-Alexander Universität Erlangen-Nürnberg, Lutz Schröder University of Erlangen-Nuremberg, Aaron Strahlberger Friedrich-Alexander-Universität Erlangen-Nürnberg
Pre-print
14:00 - 15:30
14:00
90m
Talk
Cedar: A language for expressing fast, safe, and fine-grained authorization policies
TutorialFest
Michael Hicks Amazon Web Services and the University of Maryland
14:00 - 15:30
Session 3The Future of Weak Memory at Turing Lecture
Chair(s): Brijesh Dongol University of Surrey
14:00
20m
Talk
Compilers should get over themselves and respect semantic dependencies!
The Future of Weak Memory
14:20
20m
Talk
A case against semantic dependencies
The Future of Weak Memory
Ori Lahav Tel Aviv University
14:40
20m
Talk
What Compilers desire from Weak Memory SemanticsRemote
The Future of Weak Memory
Akshay Gopalakrishnan McGill University
File Attached
15:00
20m
Talk
Programmers love mind-bogglingly complicated weak memory models
The Future of Weak Memory
File Attached
15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Afternoon Track 3TutorialFest at Flowers Room
16:00
90m
Tutorial
Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types
TutorialFest
Jonas Kastberg Hinrichsen Aarhus University, Denmark, Jules Jacobs Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
File Attached
16:00 - 17:30
Afternoon Track 1TutorialFest at Haslett Room
16:00
90m
Tutorial
Machine Learning Meets Program Synthesis
TutorialFest
Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute
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
16:00 - 17:30
Panel DiscussionPADL at Lovelace Room
Chair(s): Ekaterina Komendantskaya Heriot-Watt University and Southampton University
16:00
90m
Panel
Declarative Languages for Safe AI
PADL
P: Gopal Gupta University of Texas at Dallas, P: Wen Kokke University of Edinburgh, P: Claudia Faggian Université de Paris & CNRS, P: Alessandro Bruni IT University of Copenhagen, P: Younesse Kaddar University of Oxford
16:00 - 17:30
Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room
Chair(s): Helmut Seidl Technische Universität München
16:00
20m
Talk
Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
VMCAI
Nicolas Amat LAAS-CNRS, Silvano DAL ZILIO LAAS-CNRS, Didier Le Botlan LAAS-CNRS, INSA-Toulouse
Pre-print
16:20
20m
Talk
Parameterized Verification of Disjunctive Timed NetworksRecorded
VMCAI
Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA
16:40
20m
Talk
Resilience and Home-Space for WSTS
VMCAI
Alain Finkel ENS Paris Saclay, Mathieu Hilaire ENS Paris Saclay
17:00
20m
Talk
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
VMCAI
Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp
Pre-print
17:20
10m
Talk
TP-DejaVu: Combining Operational and Declarative Runtime Verification
VMCAI
Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki
16:00 - 17:30
16:00
90m
Talk
Cedar: A language for expressing fast, safe, and fine-grained authorization policies
TutorialFest
Michael Hicks Amazon Web Services and the University of Maryland
16:00 - 17:30
16:00
45m
Talk
A Brief Tour of Binaryen
WAW
16:45
45m
Other
Lightning Talks - please sign up!
WAW
Andreas Rossberg Independent, Conrad Watt Nanyang Technological University
16:00 - 17:30
Session 4The Future of Weak Memory at Turing Lecture
Chair(s): Brijesh Dongol University of Surrey
16:00
22m
Talk
Evolving Weak Memory Models for Evolving Architectures
The Future of Weak Memory
Reese Levine University of California at Santa Cruz
16:22
22m
Talk
In-order execution nails every weak memory behavior
The Future of Weak Memory
Chung-Kil Hur Seoul National University
16:45
22m
Talk
System-level weak memory models: The need for formalisation, ISA semantics integration and model diversity
The Future of Weak Memory
Thibaut Pérami University of Cambridge
17:07
22m
Talk
Relaxed systems semantics and how we (hope to) reason above it
The Future of Weak Memory
17:35 - 18:30
Business MeetingCPP at Kelvin Lecture
17:35
55m
Meeting
Business Meeting
CPP
Amin Timany Aarhus University, Dmitriy Traytel University of Copenhagen

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1POCL at Flowers Room
Chair(s): Peter Sewell University of Cambridge
09:00
40m
Talk
The state of Morello and CHERI
POCL
Robert N. M. Watson University of Cambridge
09:45
15m
Talk
The state of Morello software and projects
POCL
Konrad Witaszczyk University of Cambridge, UK
10:00
15m
Talk
The Morello ISA semantics, proof, and test generation
POCL
Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh
10:15
15m
Talk
Morello Cerise: proving secure encapsulation (work in progress)
POCL
Angus Hammond University of Cambridge, Ricardo Almeida University of Edinburgh
09:00 - 10:30
Keynote & Termination analysis PEPM at Haslett Room
Chair(s): Meng Wang University of Bristol
09:00
5m
Talk
Opening
PEPM
Meng Wang University of Bristol, Gabriele Keller Utrecht University
09:05
60m
Keynote
From Theory to Practice: Crafting Differential Privacy Systems with Haskell
PEPM
Alejandro Russo Chalmers University of Technology, Sweden
10:05
25m
Talk
Productivity Verification for Functional Programs by Reduction to Termination Verification
PEPM
Ren Fukaishi The University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo
DOI
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
09:00 - 10:30
Declarative Programming for AIPADL at Lovelace Room
Chair(s): Martin Gebser University of Klagenfurt, Austria
09:00
60m
Keynote
Whats and Whys of Neural Network Verification (A Declarative Programming Perspective)
PADL
K: Ekaterina Komendantskaya Heriot-Watt University and Southampton University
10:00
30m
Talk
Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks
PADL
Parth Padalkar THE UNIVERSITY OF TEXAS AT DALLAS, Huaduo Wang THE UNIVERSITY OF TEXAS AT DALLAS, Gopal Gupta University of Texas at Dallas
09:00 - 10:30
Session 5: keynote, Program and System VerificationVMCAI at Marconi Room
Chair(s): Ori Lahav Tel Aviv University
09:00
60m
Keynote
Automating Relational Verification of Infinite-State Programs
VMCAI
Hiroshi Unno University of Tsukuba
10:00
20m
Talk
Deductive Verification of Parameterized Embedded Systems modeled in SystemC
VMCAI
Philip Tasche University of Twente, Raúl E. Monti University of Twente, Stefanie Eva Drerup University of Münster, Pauline Blohm Uni Münster, Paula Herber University of Munster, Germany, Marieke Huisman University of Twente
10:20
10m
Talk
Automatically Enforcing Rust Trait Properties
VMCAI
Twain Byrnes Carnegie Mellon University, Yoshiki Takashima Carnegie Mellon University, Limin Jia Carnegie Mellon University
09:00 - 10:30
OpeningIncorrectness at Mountbatten Exhibition
Chair(s): Noam Zilberstein Cornell University
09:00
5m
Day opening
Welcome
Incorrectness
Noam Zilberstein Cornell University, Azalea Raad Imperial College London
09:05
60m
Keynote
My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
Incorrectness
Peter W. O'Hearn Lacework; University College London
10:05
22m
Talk
A Comparison of Program Logics for (In)Correctness
Incorrectness
Flavio Ascari University of Pisa
Pre-print File Attached
09:00 - 10:30
First SessionPLMW @ POPL at Turing Lecture
09:00
10m
Day opening
Opening
PLMW @ POPL
Derek Dreyer MPI-SWS
09:10
35m
Social Event
Ice Breaker
PLMW @ POPL

09:45
45m
Talk
The Evolution of Effects
PLMW @ POPL
Nicolas Wu Imperial College London
10:30 - 11:00
10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Session 2POCL at Flowers Room
Chair(s): Ian Stark The University of Edinburgh
11:00
22m
Talk
Compartmentalisation models
POCL
Dapeng Gao University of Cambridge
11:22
23m
Talk
Proving capability safety in the presence of indirect sentries
POCL
Bastien Rousseau Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Dominique Devriese KU Leuven, Jean Pichon-Pharabod Aarhus University, Lars Birkedal Aarhus University
11:45
22m
Talk
Sealed with a Library Call: Memory Allocators Should Track Capability Seal Operations
POCL
Jeremy Singer University of Glasgow
File Attached
12:08
22m
Talk
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
POCL
Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel Vrije Universiteit Brussel, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven
11:00 - 12:30
Program Inversion & DSLsPEPM at Haslett Room
Chair(s): Youyou Cong Tokyo Institute of Technology
11:00
25m
Talk
Complete Stream Fusion for Software-Defined RadioDistinguished Paper
PEPM
Tomoaki Kobayashi Tohoku University, Oleg Kiselyov Tohoku University
DOI
11:25
25m
Talk
A Case Study in Functional Conversion and Mode Inference in miniKanren
PEPM
Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen, Igor Engel JetBrains Research; Constructor University Bremen, Daniil Berezun JetBrains Research; Constructor University Bremen
DOI
11:50
25m
Talk
Partial Evaluation of Reversible Flowchart Programs
PEPM
Louis Marott Normann University of Copenhagen, Robert Glück University of Copenhagen
DOI
12:15
15m
Talk
Towards a Language-parametric DSL for Refactoring (Short Paper)
PEPM
Casper Bach Poulsen Delft University of Technology, Xulei Liu Delft University of Technology, Luka Miljak Delft University of Technology
File Attached
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
11:00 - 12:30
Session 6: Abstract InterpretationVMCAI at Marconi Room
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
11:00
20m
Talk
Formal Runtime Error Detection During Development in the Automotive Industry
VMCAI
Jesko Hecking-Harbusch Bosch Research, Jochen Quante Bosch Research, Maximilian Schlund Bosch Research
Pre-print
11:20
20m
Talk
Abstract Interpretation-Based Feature Importance for Support Vector Machines
VMCAI
Abhinandan Pal University of Birmingham, Francesco Ranzato University of Padova, Caterina Urban Inria & École Normale Supérieure | Université PSL, Marco Zanella University of Padova, Italy
11:40
20m
Talk
Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
VMCAI
Marco Milanese Sorbonne University, Antoine Miné Sorbonne Université
Pre-print
12:00
20m
Talk
Correctness Witness Validation by Abstract Interpretation
VMCAI
Simmo Saan University of Tartu, Estonia, Michael Schwarz Technische Universität München, Julian Erhard Technical University of Munich, Helmut Seidl Technische Universität München, Sarah Tilscher Technische Universität München, Vesal Vojdani University of Tartu
DOI Pre-print
11:00 - 12:30
Logics and Program AnalysisIncorrectness at Mountbatten Exhibition
Chair(s): Noam Zilberstein Cornell University
11:00
22m
Talk
Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Incorrectness
Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Nat Karmios Imperial College London, Seung Hoon Park Imperial College London, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London
Pre-print
11:22
22m
Talk
The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
Incorrectness
Caroline Cronjäger Vrije Universiteit Amsterdam
Pre-print
11:45
22m
Talk
Work in Progress: Modelling Incorrect Programs in the Open World with Dafny
Incorrectness
James Noble Creative Research & Programming, Tobias Wrigstad Uppsala University, Susan Eisenbach Imperial College London
File Attached
12:07
22m
Talk
Hoare-Like Triples and Kleene Algebras with Top and Tests
Incorrectness
Lena Verscht Saarland University, Saarland Informatics Campus, Benjamin Lucien Kaminski Saarland University; University College London
Pre-print File Attached
11:00 - 12:30
Second SessionPLMW @ POPL at Turing Lecture
Chair(s): Leonidas Lampropoulos University of Maryland, College Park
11:00
45m
Talk
Refinement Types from Light to Deep Verification
PLMW @ POPL
Niki Vazou IMDEA Software Institute
11:45
45m
Panel
Panel
PLMW @ POPL
Leonidas Lampropoulos University of Maryland, College Park, Derek Dreyer MPI-SWS, Jules Jacobs Radboud University Nijmegen, Niki Vazou IMDEA Software Institute, Sam Westrick Carnegie Mellon University
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Session 3POCL at Flowers Room
Chair(s): Simon W. Moore University of Cambridge
14:00
22m
Talk
Morello software and compilers
POCL
Jessica Clarke University of Cambridge
14:22
22m
Talk
CHERI C semantics
POCL
Vadim Zaliva University of Cambridge, UK
14:45
22m
Talk
CHERI static analysis
POCL
Irina Dudina University of Edinburgh
15:07
22m
Talk
ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
POCL
Franz Brausse The University of Manchester, Kunjian Song The University of Manchester, Fedor Shmarov The University of Manchester, Rafael Menezes University of Manchester, Mikhail R. Gadelha Igalia, Konstantin Korovin University of Manchester, Giles Reger University of Manchester, Lucas C. Cordeiro University of Manchester, UK
14:00 - 15:30
Types & Staging PEPM at Haslett Room
Chair(s): Gabriele Keller Utrecht University
14:00
25m
Talk
An Intrinsically Typed Compiler for Algebraic Effect Handlers
PEPM
Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
DOI
14:25
25m
Talk
Ownership Types for Verification of Programs with Pointer Arithmetic
PEPM
Izumi Tanaka University of Tokyo, Ken Sakayori University of Tokyo, Naoki Kobayashi University of Tokyo
DOI
14:50
25m
Talk
Scoped and Typed Staging by EvaluationRemote
PEPM
Guillaume Allais University of Strathclyde
DOI Pre-print
15:15
15m
Talk
One-Pass CPS Translation of Dependent Types (Talk Proposal)
PEPM
Youyou Cong Tokyo Institute of Technology
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
14:00 - 15:30
Answer Set Programming IIPADL at Lovelace Room
Chair(s): Mario Alviano University of Calabria
14:00
30m
Talk
Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
PADL
Yankai Zeng The University of Texas at Dallas, Abhiramon Rajasekharan The University of Texas at Dallas, Parth Padalkar THE UNIVERSITY OF TEXAS AT DALLAS, Kinjal Basu IBM, Joaquín Arias Universidad Rey Juan Carlos, Gopal Gupta University of Texas at Dallas
14:30
30m
Talk
Forgetting Techniques for Optimizing ASP-based Stream Reasoning
PADL
Francesco Calimeri University of Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Simona Perri University of Calabria, Italy, Jessica Zangari Università della Calabria
14:00 - 15:30
Session 7: Probabilistic and Quantum Programs, Neural NetworksVMCAI at Marconi Room
Chair(s): Andreas Podelski University of Freiburg
14:00
20m
Talk
Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
VMCAI
Michele Boreale Università di Firenze, Luisa Collodi University of Florence
14:20
20m
Talk
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
VMCAI
Yuxin Deng East China Normal University, Huiling Wu East China Normal University, Ming Xu East China Normal University
14:40
20m
Talk
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
VMCAI
Jiaxu Tian East China Normal University, Dapeng Zhi East China Normal University, Si Liu ETH Zurich, Peixin Wang University of Oxford, Guy Katz Hebrew University, Min Zhang East China Normal University
15:00
20m
Talk
Verification of Neural Networks’ Local Differential Classification Privacy
VMCAI
Roie Reshef Technion, Anan Kabaha Technion, Israel Institute of Technology, Olga Seleznova Technion, Dana Drachsler Cohen Technion
15:20
10m
Talk
AGNES: Abstraction-guided Framework for Deep Neural Networks Security
VMCAI
14:00 - 15:30
Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
14:00
22m
Talk
Quantitative Weakest Hyper Pre
Incorrectness
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London
File Attached
14:22
23m
Talk
A Reachability Logic for a Weak Memory Model with Promises
Incorrectness
Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg
File Attached
14:45
22m
Talk
Towards Temporal Adversarial Logic
Incorrectness
Julien Vanegue Bloomberg, USA
15:07
22m
Talk
Finding counterexamples to ∀∃ hyperproperties
Incorrectness
DOI Pre-print
14:00 - 15:30
Third SessionPLMW @ POPL at Turing Lecture
Chair(s): Andrew K. Hirsch University at Buffalo, SUNY
14:00
45m
Talk
The Potential of Information-Flow Control Research for helping GDPR Compliance
PLMW @ POPL
Alejandro Russo Chalmers University of Technology, Sweden
14:45
45m
Talk
Consider Collaboration
PLMW @ POPL
Harrison Goldstein University of Pennsylvania, Samantha Frohlich University of Bristol
15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Session 4POCL at Flowers Room
Chair(s): Brian Campbell University of Edinburgh
16:00
22m
Talk
Rust on Morello
POCL
Sarah Harris University of Kent, Simon Cooksey NVIDIA, Michael Vollmer University of Kent, Mark Batty University of Kent
16:22
22m
Talk
Capabilities for safe cross-language interoperability
POCL
David Chisnall SCI Semiconductor
16:45
22m
Talk
Concurrent Mutation must go
POCL
Matthew J. Parkinson Microsoft Azure Research, Sylvan Clebsch Microsoft Azure Research, Tobias Wrigstad Uppsala University, Sophia Drossopoulou Imperial College London, Elias Castegren KTH Royal Institute of Technology, Ellen Arvidsson Uppsala University, Luke Cheeseman Imperial College London
17:07
22m
Talk
Object Capabilities
POCL
Sophia Drossopoulou Imperial College London, Susan Eisenbach Imperial College London, Julian Mackay Victoria University of Wellington, James Noble Creative Research & Programming
16:00 - 18:30
History of PEPMPEPM at Haslett Room
Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
16:00
30m
Talk
In memoriam Neil Deaton Jones
PEPM
Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
DOI
16:30
30m
Talk
The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Contribution)
PEPM
Peter Sestoft IT University of Copenhagen, Harald Sondergaard The University of Melbourne
DOI
17:00
30m
Talk
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
PEPM
Alberto Pettorossi University of Rome Tor Vergata; IASI-CNR, Maurizio Proietti IASI-CNR, Fabio Fioravanti University of Chieti-Pescara, Emanuele De Angelis IASI-CNR
DOI
17:30
30m
Talk
Incremental Computation: What Is the Essence? (Invited Contribution)Remote
PEPM
Y. Annie Liu Stony Brook University
DOI
18:00
30m
Meeting
Informal discussion on history and future of PEPM
PEPM

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
16:00 - 17:30
Session 8: Concurrency, Program and System Verification, ClosingVMCAI at Marconi Room
Chair(s): Viktor Kunčak EPFL, Switzerland
16:00
20m
Talk
Petrification: Software Model Checking for Programs with Dynamic Thread Management
VMCAI
Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Lars Nitzke University of Freiburg, Frank Schüssele University of Freiburg
Pre-print
16:20
20m
Talk
A Fully Verified Persistency Library
VMCAI
Stefan Bodenmüller University of Augsburg, John Derrick , Brijesh Dongol University of Surrey, Gerhard Schellhorn Universitaet Augsburg, Heike Wehrheim University of Oldenburg
16:40
20m
Talk
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
VMCAI
Roman Lakenbrink University of Münster, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster, Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany
Pre-print
17:00
20m
Talk
Borrowable Fractional Ownership Types for Verification
VMCAI
Takashi Nakayama The University of Tokyo, Yusuke Matsushita The University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo
Pre-print
17:20
10m
Day closing
Closing (+ best paper award announcement)
VMCAI

16:00 - 17:30
TypesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
16:00
22m
Talk
Type-Based Incorrectness Reasoning
Incorrectness
Zhe Zhou Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
16:23
22m
Talk
Ill-Typed Programs Don't Evaluate
Incorrectness
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol
16:00 - 17:30
Fourth SessionPLMW @ POPL at Turing Lecture
Chair(s): Hannah Gommerstadt Vassar College
16:00
45m
Talk
How to Give a Talk
PLMW @ POPL
Neel Krishnaswami University of Cambridge
16:45
45m
Talk
Managing undergraduate research, as mentor and mentee
PLMW @ POPL
Mae Milano Princeton University
18:00 - 21:30
18:00
3h30m
Social Event
Jane Street Board Game Night
PLMW @ POPL
Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street

Wed 17 Jan

Displayed time zone: London change

08:25 - 08:45
Wednesday Morning Sessions PreviewsSession Previews at Siemens Boardroom
Chair(s): Clément Pit-Claudel EPFL
08:25
10m
Research preview
Synthesis 1: Session Preview
Session Previews
Xiaokang Qiu Purdue University
08:35
10m
Research preview
Types 1: Session Preview
Session Previews
Niki Vazou IMDEA Software Institute
08:50 - 09:00
Welcome from the ChairPOPL at Kelvin Lecture +0min
08:50 - 09:00
Welcome from the ChairPOPL at Turing Lecture
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:05 - 10:25
Wednesday Morning Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Ariel E. Kellison Cornell University
10:05
10m
Research preview
Effect Handlers: Session Preview
Session Previews
Sam Lindley University of Edinburgh
10:15
10m
Research preview
Automated Verification: Session Preview
Session Previews
Viktor Kunčak EPFL, Switzerland
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
10:30 - 11:50
Types 1POPL at Turing Lecture
Chair(s): Mae Milano Princeton University
10:30
20m
Talk
Generating Well-Typed Terms that are not "Useless"
POPL
Justin Frank University of Maryland, College Park, Benjamin Quiring University of Maryland, Leonidas Lampropoulos University of Maryland, College Park
10:50
20m
Talk
Indexed Types for a Statically Safe WebAssembly
POPL
Adam Geller Computer Science, University of British Columbia, Justin Frank University of Maryland, College Park, William J. Bowman University of British Columbia
DOI Pre-print
11:10
20m
Talk
The Essence of Generalized Algebraic Data TypesRemote
POPL
Filip Sieczkowski Heriot-Watt University, Sergei Stepanenko Aarhus University, Jonathan Sterling University of Cambridge, Lars Birkedal Aarhus University
11:30
20m
Talk
Ill-Typed Programs Don't Evaluate
POPL
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol
11:50 - 13:20
11:50
90m
Lunch
URM Lunch
Diversity, Equity and Inclusion

12:50 - 13:10
Wednesday Lunch Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Aurèle Barrière EPFL
12:50
10m
Research preview
Automata and Complexity: Session Preview
Session Previews
Benjamin Lucien Kaminski Saarland University; University College London
13:00
10m
Research preview
Separation Logic: Session Preview
Session Previews
Ralf Jung ETH Zurich
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
Oisín Kidney Imperial College London, Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
Pre-print
13:20 - 14:40
Automated VerificationPOPL at Turing Lecture
Chair(s): Gregory Malecha BedRock Systems
13:20
20m
Talk
Regular Abstractions for Array Systems
POPL
Chih-Duo Hong National Chengchi University, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
13:40
20m
Talk
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper
POPL
Neta Elad Tel Aviv University, Oded Padon VMware Research, Sharon Shoham Tel Aviv University
Link to publication DOI
14:00
20m
Talk
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
POPL
Jianan Yao Columbia University, Runzhou Tao Columbia University, Ronghui Gu Columbia University, Jason Nieh Columbia University
14:20
20m
Talk
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP
14:45 - 15:05
Wednesday Afternoon Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Samantha Frohlich University of Bristol
14:45
10m
Research preview
Concurrency: Session Preview
Session Previews
Shaz Qadeer Meta, Inc.
14:55
10m
Research preview
Domain-Specific Languages: Session Preview
Session Previews
John Wickerson Imperial College London
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
15:10 - 16:30
Separation LogicPOPL at Turing Lecture
Chair(s): Azalea Raad Imperial College London
15:10
20m
Talk
An Iris Instance for Verifying CompCert C Programs
POPL
William Mansky University of Illinois Chicago, Ke Du
Pre-print
15:30
20m
Talk
The Logical Essence of Well-Bracketed Control Flow
POPL
Amin Timany Aarhus University, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Lars Birkedal Aarhus University
15:50
20m
Talk
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL
Simon Oddershede Gregersen Aarhus University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti NYU, Lars Birkedal Aarhus University
DOI Pre-print
16:10
20m
Talk
Thunks and Debits in Separation Logic with Time Credits
POPL
François Pottier Inria, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan CNR, LMF, Glen Mével
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
16:50 - 18:10
Domain-Specific LanguagesPOPL at Turing Lecture
Chair(s): Satnam Singh Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Yuqi Chen ShanghaiTech University, China, Taolue Chen University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton Brown University, Shriram Krishnamurthi Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche Université Paris-Dauphine -- PSL, Mohamed-Amine Baazizi Sorbonne Université, Dario Colazzo Université Paris-Dauphine -- PSL, Giorgio Ghelli Universita di Pisa, Carlo Sartiani Università della Basilicata, Stefanie Scherzinger Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin The University of Edinburgh, Liam O'Connor University of Edinburgh, Rob van Glabbeek The University of Edinburgh, Peter Hoefner Australian National University, Ohad Kammar University of Edinburgh, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
18:10 - 20:00
POPL Networking ReceptionPOPL at Maxwell Library
18:10
1h50m
Social Event
POPL Networking Reception
POPL

18:10 - 20:00
POPL Networking ReceptionPOPL at Riverside Room
18:10
1h50m
Social Event
POPL Networking Reception
POPL

18:15 - 20:00
18:15
4m
Poster
A Denotational Approach to Release/Acquire Concurrency
Student Research Competition
Yotam Dvir Tel Aviv University
18:19
4m
Talk
A Lean Formalization of Cedar
Student Research Competition
Bhakti Shah University of Chicago
18:24
4m
Talk
A Substructural Type and Effect System
Student Research Competition
Orpheas van Rooij Radboud University
18:29
4m
Poster
A type-safe generalized editor calculus (Extended Abstract)
Student Research Competition
Nikolaj Rossander Kristensen Department of Computer Science, Aalborg University, Benjamin Bennetzen Department of Computer Science, Aalborg University, Peter Buus Steffensen Department of Computer Science, Aalborg University, Andreas Tor Mortensen Department of Computer Science, Aalborg University
18:34
4m
Poster
Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
Student Research Competition
Vince Szabó Delft University of Technology
18:38
4m
Poster
Compositional Programming with Full Iso-recursive Types
Student Research Competition
Litao Zhou Shanghai Jiao Tong University; University of Hong Kong
18:43
4m
Poster
Differential Privacy in an Impure World
Student Research Competition
Damián Arquez University of Chile
18:48
4m
Poster
Effect handlers in Zig (extended abstract)
Student Research Competition
Alessio Duè University of Pisa
18:53
4m
Talk
Efficient Incremental Computation for Halide
Student Research Competition
Tyler Hou University of California, Berkeley
Pre-print
18:57
4m
Talk
Embedding Pointful Array Programming in Python
Student Research Competition
Jakub Bachurski University of Cambridge
19:02
4m
Poster
Exploring the limitations of Contextual Modal Type Theory for Multi-Stage Programming
Student Research Competition
Theo Wang University of Oxford
19:07
4m
Poster
From Java to Kotlin with Contextual Equality Saturation
Student Research Competition
19:12
4m
Poster
GPU-Accelerated Synthesis of Boolean Circuits
Student Research Competition
Justin Du University of California, San Diego, Rana Lulla University of California San Diego, Melody Ruth University of California San Diego
19:17
4m
Talk
HOL4P4: A Heapless Small-Step Semantics and Type System for P4
Student Research Competition
Anoud Alshnakat KTH Royal Institute of Technology, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH
19:21
4m
Poster
Linking Session-Typed Channels in Separation Logic
Student Research Competition
Thomas Somers Radboud University
19:26
4m
Poster
Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
19:31
4m
Poster
Optimization of the Context-Free Language Reachability Matrix-Based Algorithm
Student Research Competition
Ilya Muravjov Saint Petersburg State University
19:36
4m
Poster
PiR (πr): Probabilistic Interpretation of Robustness
Student Research Competition
Abhinandan Pal University of Birmingham
19:40
4m
Talk
Session-Typed Effect Handlers
Student Research Competition
Wenhao Tang University of Edinburgh
19:45
4m
Poster
Tail: A Typed and Structured Document Editor
Student Research Competition
Alperen Keles University of Maryland at College Park
19:50
4m
Poster
Towards programmatic reinforcement learning: the case of deterministic gridworlds
Student Research Competition
Guruprerana Shabadi École Polytechnique, Institut Polytechnique de Paris
19:55
4m
Poster
Zero-Cost Capabilities: Retrofitting Effect Safety in Rust
Student Research Competition
George Berdovskiy University of California, Davis

Thu 18 Jan

Displayed time zone: London change

08:30 - 08:50
Thursday Breakfast Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Lydia Kondyludou
08:30
10m
Research preview
Synthesis 2: Session Preview
Session Previews
Hila Peleg Technion
08:40
10m
Research preview
Higher-Order Effectful Programs: Session Preview
Session Previews
Andrew K. Hirsch University at Buffalo, SUNY
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
09:00 - 10:20
Higher-Order Effectful ProgramsPOPL at Turing Lecture
Chair(s): Sam Lindley University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Alexis Ghyselen University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman University of Copenhagen, Denmark
Link to publication DOI
09:40
20m
Talk
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Harrison Grodin , Jonathan Sterling University of Cambridge, Yue Niu Carnegie Mellon University, Robert Harper Carnegie Mellon University
Pre-print
10:00
20m
Talk
Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote
POPL
Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI Pre-print
10:25 - 10:45
Thursday Morning Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Gabriele Vanoni IRIF, Université Paris Cité
10:25
10m
Research preview
Types 2: Session Preview
Session Previews
10:35
10m
Research preview
Probabilistic Programs: Session Preview
Session Previews
Jules Jacobs Radboud University Nijmegen
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
10:50 - 12:10
Probabilistic ProgramsPOPL at Turing Lecture
Chair(s): Jules Jacobs Radboud University Nijmegen
10:50
20m
Talk
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
POPL
Nate Ackerman Harvard University, Cameron Freer Massachusetts Institute of Technology, Younesse Kaddar University of Oxford, Jacek Karwowski University of Oxford, Sean Moss University of Oxford, Daniel Roy University of Toronto, Sam Staton University of Oxford, Hongseok Yang KAIST; IBS
11:10
20m
Talk
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL
Francesca Randone IMT School for Advanced Studies Lucca, Luca Bortolussi Department of Mathematics and Geosciences, University of Trieste, Emilio Incerto IMT School for Advanced Studies Lucca, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy
11:30
20m
Talk
Higher Order Bayesian Networks, Exactly
POPL
Claudia Faggian Université de Paris & CNRS, Daniele Pautasso Università di Torino, Gabriele Vanoni IRIF, Université Paris Cité
11:50
20m
Talk
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL
12:10 - 13:40
12:10
90m
Lunch
LGBTQ+ Lunch
Diversity, Equity and Inclusion

12:10 - 13:40
12:10
90m
Lunch
Mentoring Lunch
Diversity, Equity and Inclusion

13:10 - 13:30
Thursday Lunch Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Lucy Menon Northeastern University
13:10
10m
Research preview
Quantum Computing: Session Preview
Session Previews
Oded Padon VMware Research
13:20
10m
Research preview
Weak Memory and Concurrent Separation Logic: Session Preview
Session Previews
Mike Dodds Galois, Inc.
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
13:40 - 15:00
Weak Memory and Concurrent Separation LogicPOPL at Turing Lecture
Chair(s): William Mansky University of Illinois Chicago
13:40
20m
Talk
How Hard is Weak-Memory Testing?
POPL
Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
Pre-print
14:00
20m
Talk
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Angus Hammond University of Cambridge, Zongyuan Liu Aarhus University, Thibaut Pérami University of Cambridge, Peter Sewell University of Cambridge, Lars Birkedal Aarhus University, Jean Pichon-Pharabod Aarhus University
Pre-print
14:20
20m
Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Amin Timany Aarhus University, Simon Oddershede Gregersen Aarhus University, Leo Stefanesco MPI-SWS, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Léon Gondelman Aarhus University, Abel Nieto Aarhus University, Lars Birkedal Aarhus University
14:40
20m
Talk
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen
Pre-print
15:05 - 15:25
Thursday Afternoon Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Son Ho INRIA
15:05
10m
Research preview
Parallelism: Session Preview
Session Previews
John Reppy University of Chicago, USA
15:15
10m
Research preview
Algorithmic Verification: Session Preview
Session Previews
Konstantinos Mamouras Rice 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
15:30 - 16:50
15:30
13m
Talk
Embedding Pointful Array Programming in Python
Student Research Competition
Jakub Bachurski University of Cambridge
15:43
13m
Talk
A Lean Formalization of Cedar
Student Research Competition
Bhakti Shah University of Chicago
15:56
13m
Talk
Efficient Incremental Computation for Halide
Student Research Competition
Tyler Hou University of California, Berkeley
Pre-print
16:10
13m
Talk
A Substructural Type and Effect System
Student Research Competition
Orpheas van Rooij Radboud University
16:23
13m
Talk
Session-Typed Effect Handlers
Student Research Competition
Wenhao Tang University of Edinburgh
16:36
13m
Talk
HOL4P4: A Heapless Small-Step Semantics and Type System for P4
Student Research Competition
Anoud Alshnakat KTH Royal Institute of Technology, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH
15:30 - 16:50
Algorithmic VerificationPOPL at Turing Lecture
Chair(s): Andreas Pavlogiannis Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk Warsaw University, Bartek Klin University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
Pre-print
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

18:30 - 20:00
18:30
90m
Social Event
DEI4Everyone Reception
Diversity, Equity and Inclusion

Fri 19 Jan

Displayed time zone: London change

08:25 - 08:45
Friday Breakfast Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Xulei Liu Delft University of Technology
08:25
10m
Research preview
Program Analysis: Session Preview
Session Previews
Roberto Giacobazzi University of Arizona, Tucson, Arizona, USA
08:35
10m
Research preview
Type Theory: Session Preview
Session Previews
Kuen-Bang Hou (Favonia) University of Minnesota
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
08:50 - 09:00
WelcomePOPL at Turing Lecture
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:05 - 10:25
Friday Morning Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Aleksander Boruch-Gruszecki EPFL
10:05
10m
Research preview
Types 3: Session Preview
Session Previews
10:15
10m
Research preview
Medley: Session Preview
Session Previews
Philip Wadler University of Edinburgh
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
10:30 - 11:50
Type TheoryPOPL at Turing Lecture
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
10:30
20m
Talk
Internal parametricity, without an interval
POPL
Thorsten Altenkirch University of Nottingham, Yorgo Chamoun École Polytechnique, Ambrus Kaposi Eötvös Loránd University, Michael Shulman University of San Diego
Pre-print
10:50
20m
Talk
Internal and Observational Parametricity for Cubical Agda
POPL
Antoine Van Muylder KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
11:10
20m
Talk
Internalizing Indistinguishability with Dependent TypesRemote
POPL
Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Jessica Shi University of Pennsylvania, Stephanie Weirich University of Pennsylvania
11:30
20m
Talk
Polynomial Time and Dependent types
POPL
Robert Atkey University of Strathclyde
11:50 - 13:20
11:50
90m
Lunch
Women Lunch
Diversity, Equity and Inclusion

12:50 - 13:10
Friday Lunch Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Ekaterina Zhuchko Tallinn University of Technology
12:50
10m
Research preview
Machine and Automata Learning: Session Preview
Session Previews
Steven Holtzen Northeastern University
13:00
10m
Research preview
Mechanized Proofs: Session Preview
Session Previews
Sandrine Blazy University of Rennes
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 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
13:20 - 14:40
MedleyPOPL at Turing Lecture
Chair(s): Xiaokang Qiu Purdue University
13:20
20m
Talk
Guided Equality Saturation
POPL
Thomas Koehler INRIA, Andrés Goens University of Amsterdam, Siddharth Bhat the University of Edinburgh, Tobias Grosser University of Edinburgh, Phil Trinder University of Glasgow, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
13:40
20m
Talk
Fusing Direct Manipulations into Functional Programs
POPL
Xing Zhang Peking University, Ruifeng Xie Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Tao Zan Longyan University, Zhenjiang Hu Peking University
Pre-print
14:00
20m
Talk
Inference of Robust Reachability Constraints
POPL
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Guillaume Girol CEA, List, Université Paris Saclay, Frédéric Recoules CEA, List, Damien Couroussé Univ Grenoble Alpes, CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:20
20m
Talk
Nominal Recursors as Epi-RecursorsDistinguished Paper
POPL
Andrei Popescu University of Sheffield
14:45 - 15:05
Friday Afternoon Session PreviewsSession Previews at Siemens Boardroom
Chair(s): Paulette Koronkevich University of British Columbia
14:45
10m
Research preview
Gradual Typing and Verification: Session Preview
Session Previews
Ronald Garcia University of British Columbia
14:55
10m
Research preview
Logical Foundations: Session Preview
Session Previews
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
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
15:10 - 16:30
Mechanized ProofsPOPL at Turing Lecture
Chair(s): Andrei Popescu University of Sheffield
15:10
20m
Talk
Mechanizing Refinement Types
POPL
Michael Borkowski University of California, San Diego, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego
15:30
20m
Talk
VST-A: A Foundationally Sound Annotation Verifier
POPL
Litao Zhou Shanghai Jiao Tong University; University of Hong Kong, Jianxing Qin Shanghai Jiao Tong University, Qinshi Wang Princeton University, Andrew W. Appel Princeton University, Qinxiang Cao Shanghai Jiao Tong University
15:50
20m
Talk
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Jinhua Wu Shanghai Jiao Tong University, Jérémie Koenig Yale University, Zhong Shao Yale University
Pre-print
16:10
20m
Talk
A Formalization of Core Why3 in Coq
POPL
Joshua M. Cohen Princeton University, Philip Johnson-Freyd Sandia National Laboratories
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, Theo Winterhalter INRIA Saclay
Pre-print
17:10
20m
Talk
Sound Gradual Verification with Symbolic Execution
POPL
Conrad Zimmerman Brown University, Jenna Wise (DiVincenzo) 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
16:50 - 17:50
Logical FoundationsPOPL at Turing Lecture
Chair(s): Emanuele D’Osualdo MPI-SWS
16:50
20m
Talk
Orthologic with Axioms
POPL
Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland
Pre-print
17:10
20m
Talk
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster
Pre-print
17:30
20m
Talk
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Patrick Cousot New York University
18:10 - 18:15
Farewell from the ChairPOPL at Kelvin Lecture +0min
18:10 - 18:15
Farewell from the ChairPOPL at Turing Lecture

Sat 20 Jan

Displayed time zone: London change

09:00 - 10:30
KeynotePROPL at Flowers Room
Chair(s): Anil Madhavapeddy University of Cambridge, UK
09:00
45m
Keynote
Setting the stage for AI for biodiversity
PROPL
Drew Purves Google DeepMind
09:45
45m
Keynote
Building Open Source Software for Climate Change Research — Lessons Learned from Mimi.jlRemote
PROPL
Lisa Rennels University of California at Berkeley
09:00 - 10:30
Session 1WITS at Haslett Room
Chair(s): Richard A. Eisenberg Jane Street
09:00
60m
Keynote
Inside the Scala Capture Checker
WITS
10:00
30m
Talk
Binding Syntax for Dependently-Typed Programs
WITS
Andre Videla University Of Strathclyde
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
09:00 - 10:30
Quantum TypesPLanQC at Marconi Room
Chair(s): Mathys Rennela INRIA Paris
09:00
45m
Keynote
Monoidal Adventures
PLanQC
Conor McBride University of Strathclyde
09:45
22m
Talk
Introducing BRAT
PLanQC
Ross Duncan Quantinuum, Mark Koch Quantinuum, Alan Lawrence Quantinuum, Conor McBride University of Strathclyde, Craig Roy Quantinuum
File Attached
10:07
22m
Talk
Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract)
PLanQC
Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis
09:00 - 10:30
Invited Talks 1N40AI at Siemens Boardroom
Chair(s): Antoine Miné Sorbonne Université
09:00
45m
Talk
Mechanizing Abstract Interpretation
N40AI
Xavier Leroy Collège de France
09:45
45m
Talk
Program Synthesis via Bi-directional Reduced-product Abstract Interpretation
N40AI
Kwangkeun Yi Seoul National University
09:00 - 10:30
Session 1PriSC at Turing Lecture
Chair(s): Marco Patrignani University of Trento
09:00
5m
Day opening
Introduction
PriSC
Shweta Shinde ETH Zurich, Marco Patrignani University of Trento
09:05
60m
Keynote
Keynote: Can we reason about the security of concurrent systems code?
PriSC
Peter Sewell University of Cambridge
10:05
25m
Talk
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
PriSC
Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel Vrije Universiteit Brussel, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven
File Attached
10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Modelling and analysis / Energy and efficiencyPROPL at Flowers Room
Chair(s): Ryan Gibb
11:00
20m
Talk
The programming challenges of climate data analysis
PROPL
Ezequiel Cimadevilla Instituto de Fisica de Cantabria
11:20
20m
Talk
Categorical Composition of Discrete Exterior Calculus Climate ModelsRemote
PROPL
Luke Morris University of Florida, George Rauta University of Florida, James Fairbanks University of Florida
11:40
20m
Talk
Formal Methods to Save the Earth
PROPL
Hongyi Huang National University of Singapore, Jialin Li National University of Singapore, Singapore, Umang Mathur National University of Singapore
12:00
20m
Talk
Kepler Watt Store: Kepler Software Watt Watcher StoreRemote
PROPL
PARUL SINGH RED HAT, Huamin Chen RED HAT, Christophe Laprun RED HAT
12:20
10m
Other
Discussion
PROPL

11:00 - 12:30
Session 2WITS at Haslett Room
Chair(s): William J. Bowman University of British Columbia
11:00
30m
Talk
Retrofitting Null-Safety into Java
WITS
Artem Pianykh Facebook London
12:00
30m
Talk
Type inference for application spines
WITS
Simon Peyton Jones Epic Games
11:00 - 12:30
CompilationPLanQC at Marconi Room
Chair(s): Ross Duncan Quantinuum
11:00
22m
Talk
Graphical Primitive Recursion For String Diagrams
PLanQC
Zhulien Zhelezchev University of Bristol, Aleks Kissinger University of Oxford
11:22
22m
Talk
Optimal compilation of parametrised quantum circuits
PLanQC
John van de Wetering University of Amsterdam, Richie Yeung University of Oxford, Tuomas Laakkonen Quantinuum, Aleks Kissinger University of Oxford
11:45
22m
Talk
Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Function Algorithm
PLanQC
Lucas Stinchcombe Simon Fraser University, Matthew Amy Simon Fraser University
12:07
22m
Talk
Qadence: a differentiable interface for digital-analog programs
PLanQC
Dominik Seitz PASQAL SAS, Niklas Heim PASQAL SAS, João P. Moutinho PASQAL SAS, Roland Guichard PASQAL SAS, Vytautas Abramavicius PASQAL SAS, Aleksander Wennersteen PASQAL SAS, Gert-Jan Both PASQAL SAS, Mario Dagrada PASQAL SAS, Vincent Elfving PASQAL SAS
Pre-print File Attached
11:00 - 12:30
Invited Talks 2N40AI at Siemens Boardroom
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
11:00
45m
Talk
Quantum Abstract Interpretation
N40AI
Jens Palsberg University of California, Los Angeles (UCLA)
11:45
45m
Talk
Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
N40AI
Mooly Sagiv Tel Aviv University
File Attached
11:00 - 12:30
Session 2PriSC at Turing Lecture
Chair(s): Marco Vassena Utrecht University
11:00
22m
Talk
Microarchitectural Side-Channel Mitigations for Serverless Applications
PriSC
Yayu Wang The University of British Columbia, Aastha Mehta The University of British Columbia
File Attached
11:22
22m
Talk
Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
PriSC
Xaver Fabian Cispa Helmholtz Center for Information Security, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
11:45
22m
Talk
Secure Composition of SPECTRE Mitigations
PriSC
Matthis Kruse CISPA Helmholtz Center for Information Security, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
12:07
22m
Talk
When Obfuscations Preserve Cryptographic Constant-Time
PriSC
Matteo Busi University Ca' Foscari, Venice, Pierpaolo Degano University of Pisa and IMT School for Advanced Studies Lucca, Letterio Galletta IMT School for Advanced Studies Lucca
File Attached
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

12:30 - 14:00
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Software engineering and ecosystemsPROPL at Flowers Room
Chair(s): Michael Dales University of Cambridge, UK
14:00
20m
Talk
Assessing the availability, reproducibility and reuseability of research software
PROPL
Vashti Galpin University of Edinburgh
14:20
20m
Talk
Fluid: towards transparent, self-explanatory research outputs
PROPL
Joe Bond University of Bristol, UK, Cristina David University of Bristol, Minh Nguyen University of Bristol, Roly Perera University of Cambridge/University of Bristol
Pre-print
14:40
20m
Talk
Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine
PROPL
Alexander Bandukwala Unaffiliated, Andrew Blinn University of Michigan, Cyrus Omar University of Michigan
15:00
30m
Other
Discussion on multidisciplinary PROPL-work
PROPL
Patrick Ferris University of Cambridge, UK, Michael Dales University of Cambridge, UK
14:00 - 15:30
Session 3WITS at Haslett Room
14:00
30m
Talk
On Modelling Heap Invariants for Type Systems in Dafny
WITS
James Noble Creative Research & Programming, Tobias Wrigstad Uppsala University
14:30
30m
Talk
Solving constraints during type inference
WITS
Simon Peyton Jones Epic Games
15:00
30m
Talk
Yaffle: A New Core for Idris 2
WITS
Edwin Brady University of St Andrews, UK
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
14:00 - 15:30
New Directions for Quantum ProgrammingPLanQC at Marconi Room
Chair(s): Aleks Kissinger University of Oxford
14:00
22m
Talk
A feasible and unitary programming language with quantum control
PLanQC
Alejandro Díaz-Caro ICC (UBA-CONICET) & UNQ, Emmanuel Hainry LORIA, Université de Lorraine, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA, Mário Silva LORIA, Université de Lorraine
14:22
22m
Talk
GUPPY: Pythonic Quantum-Classical Programming
PLanQC
Mark Koch Quantinuum, Alan Lawrence Quantinuum, Kartik Singhal Quantinuum, Seyon Sivarajah Quantinuum, Ross Duncan Quantinuum
Media Attached File Attached
14:44
22m
Talk
Quantum and Classical Control (work-in-progress)remote
PLanQC
Kinnari Dave Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Louis Lemonnier Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA, Vladimir Zamdzhiev Inria
14:00 - 15:30
Invited Talks 3N40AI at Siemens Boardroom
Chair(s): Jerome Feret INRIA Paris
14:00
45m
Talk
AI for the People
N40AI
Peter W. O'Hearn Lacework; University College London
14:45
45m
Talk
Unified Compositional Symbolic Execution
N40AI
Philippa Gardner Imperial College London
14:00 - 15:30
Session 3PriSC at Turing Lecture
Chair(s): Matteo Busi University Ca' Foscari, Venice
14:00
22m
Talk
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
PriSC
File Attached
14:22
22m
Talk
Modularizing CPU Semantics for Virtualization
PriSC
Paolo G. Giarrusso BedRock Systems, Abhishek Anand BedRock Systems, Gregory Malecha BedRock Systems, František Farka BedRock Systems, Hoang-Hai Dang BedRock Systems
File Attached
14:45
22m
Talk
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC
Andrew Wagner Northeastern University, Amal Ahmed Northeastern University, USA
File Attached
15:07
22m
Talk
Short Talks
PriSC

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Policy and decision making / BrainstormingPROPL at Flowers Room
Chair(s): Vashti Galpin University of Edinburgh
16:00
20m
Talk
Scalable agent-based models for optimized policy design: applications to the economics of biodiversity and carbon
PROPL
Sharan Agrawal University of Cambridge, UK
Link to publication
16:20
20m
Talk
Can computer science help climate policy making?Remote
PROPL
Nicola Botta Potsdam Institute for Climate Impact Research (PIK), Patrik Jansson Chalmers University of Technology and University of Gothenbrug
16:40
50m
Other
Discussion and brain storming: How can the CS/PL community help address the current planetary crises?
PROPL
Dominic Orchard University of Kent, UK and University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK
16:00 - 17:30
Session 4WITS at Haslett Room
Chair(s): Edwin Brady University of St Andrews, UK
16:00
30m
Talk
asai: a Library for Compiler Diagnostics
WITS
Kuen-Bang Hou (Favonia) University of Minnesota, Reed Mullanix McMaster University
16:30
30m
Talk
Efficient Evaluation with Controlled Definition Unfolding
WITS
András Kovács University of Gothenburg
17:00
30m
Talk
Implementing separation logic using an SMT-backed Frame RuleRemote
WITS
Kirill Golubev University of Lisbon, Alcides Fonseca University of Lisbon
16:00 - 17:30
VerificationPLanQC at Marconi Room
Chair(s): Robert Rand University of Chicago
16:00
22m
Talk
Effect Semantics for Quantum Protocols
PLanQC
Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy
16:22
22m
Talk
QbC: Quantum Correctness by Constructionremote
PLanQC
Anurudh Peduri Ruhr University Bochum, Ina Schaefer KIT, Michael Walter Ruhr-Universität Bochum
Pre-print
16:45
22m
Talk
Quantum Controlled Measurements via Program Transformation
PLanQC
Kengo Hirata University of Edinburgh, Takeshi Tsukada Chiba University
File Attached
17:07
22m
Talk
QGAT: A Generate-and-Test Paradigm for Quantum Circuits
PLanQC
Ulrik de Muelenaere University of Notre Dame
File Attached
16:00 - 17:30
Short TalksN40AI at Siemens Boardroom
Chair(s): Roberto Giacobazzi University of Arizona
16:00
90m
Talk
Short talks: Past, Present and Future of AI
N40AI
Roberto Giacobazzi University of Arizona, Eric Goubault Ecole Polytechnique, Laurent Mauborgne Absint GmbH, Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France, David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Andreas Podelski University of Freiburg, David Schmidt , Reinhard Wilhelm Saarland University
16:00 - 17:30
Session 4PriSC at Turing Lecture
Chair(s): Dominique Devriese KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna Wise (DiVincenzo) Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang BedRock Systems, David Swasey BedRock Systems, Gregory Malecha BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde ETH Zurich