Program - POPL 2025

Program - POPL 2025
POPL 2025
Sun 19 - Sat 25 January 2025
Denver, Colorado, United States
Attending
Venue: Curtis Hotel Denver
Supporting POPL
Registration
Information for Virtual Attendees
Information for Presenters
Requesting a Visa
POPL Live Streams
Code of Conduct
Program
POPL Program
Your Program
Filter by Day
Sun 19 Jan
Mon 20 Jan
Tue 21 Jan
Wed 22 Jan
Thu 23 Jan
Fri 24 Jan
Sat 25 Jan
Tracks
POPL 2025
Artifact Evaluation
POPL
Student Research Competition
Student Volunteers
Tutorials
Workshops and Co-located Events
Co-hosted Conferences
CPP
VMCAI
Workshops
CoqPL
Dafny
LAFI
PEPM
PLanQC
PLMW @ POPL
PriSC
TPSA
WAW
WITS
Co-hosted Symposia
PADL
Organization
POPL 2025 Committees
Organizing Committee
AV Committee
Student Volunteers
Track Committees
Artifact Evaluation
POPL
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CPP
Organizing Committee
Program Committee
Steering Committee
VMCAI
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Program Committee
Dafny
Program Committee Chairs
Program Committee
Steering Committee Chairs
LAFI
Program Committee
Steering Committee
PEPM
Chairs
Program Committee Members
PLanQC
Organizing Committee
Program Committee
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PriSC
Program Committee
Steering Committee
TPSA
Organizing Committee
Program Committee
WAW
Organizers
Program Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Program Committee
Series
Series
POPL 2027
POPL 2026
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
POPL 2025
series
) /
POPL 2025 Program
Detailed Table
Session Timeline
Detailed Timeline
Switch Program View
You're viewing a filtered program.
Do you want to keep these filters active in the new view?
Close
Get Calendar (iCal)
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Program Display Configuration
Close
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 19 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Keynote
Dafny
at
Hopscotch
Chair(s):
Stefan Zetzsche
Amazon Web Services
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche
Amazon Web Services
09:10
60m
Keynote
Keynote
Dafny
K. Rustan M. Leino
Amazon
09:00 - 10:30
Substructural Type Systems
Tutorials
at
Patty Cake
09:00
90m
Tutorial
Substructural Type Systems
Tutorials
P:
Frank Pfenning
Carnegie Mellon University, USA
09:00 - 10:30
First session
LAFI
at
Peek-A-Boo
Chair(s):
Matthijs Vákár
Utrecht University
09:00
5m
Day opening
Welcome
LAFI
Matthijs Vákár
Utrecht University
Atılım Güneş Baydin
University of Oxford
09:06
20m
Industry talk
Industry Talk: Basis - Programming Languages as Core Technology for AI
LAFI
Jack Feser
Basis
09:27
15m
Talk
Towards Symbolic Execution for Probability and Non-determinism
LAFI
Jack Czenszak
Northeastern University
John Li
Northeastern University
Steven Holtzen
Northeastern University
File Attached
09:43
15m
Talk
Lazy Knowledge Compilation for Discrete PPLs
LAFI
Maddy Bowers
Massachusetts Institute of Technology
Alexander K. Lew
Massachusetts Institute of Technology
Joshua B. Tenenbaum
Massachusetts Institute of Technology
Vikash K. Mansinghka
Massachusetts Institute of Technology
Armando Solar-Lezama
Massachusetts Institute of Technology
09:59
15m
Talk
Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs
LAFI
Anthony D'Arienzo
University of Illinois and Sandia National Laboratories
Jon Aytac
Sandia National Laboratories
10:15
15m
Talk
Exact Inference for Nested Discrete Probabilistic Programs (Remote)
LAFI
Francesco Pontiggia
TU Wien
Ezio Bartocci
TU Wien
Michele Chiari
TU Wien
File Attached
11:00 - 12:30
Proof Stability and Applications
Dafny
at
Hopscotch
Chair(s):
Stefan Zetzsche
Amazon Web Services
11:00
18m
Talk
Helping users to reduce Brittleness in their Dafny programs - a success story
Dafny
Remy Willems
Amazon
Matthias Schlaipfer
Amazon
Olivier Bouissou
Amazon
11:18
18m
Talk
Towards Proof Stability in SMT-based Program Verification
Dafny
Yi Zhou
Carnegie Mellon University
Bryan Parno
Carnegie Mellon University
11:36
18m
Talk
Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Dafny
Stefan Zetzsche
Amazon Web Services
Tancrède Lepoint
Amazon Web Services
Jean-Baptiste Tristan
Amazon Web Services
Mikael Mayer
Automated Reasoning Group, Amazon Web Services
Pre-print
11:54
18m
Talk
Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Dafny
Derek Leung
Massachusetts Institute of Technology, USA
Nickolai Zeldovich
Massachusetts Institute of Technology, USA
M. Frans Kaashoek
Massachusetts Institute of Technology, USA
12:12
18m
Talk
Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
Dafny
Stefan Zetzsche
Amazon Web Services
Wojciech Różowski
University College London
11:00 - 12:30
Substructural Type Systems
Tutorials
at
Patty Cake
11:00
90m
Tutorial
Substructural Type Systems
Tutorials
P:
Frank Pfenning
Carnegie Mellon University, USA
11:00 - 12:30
Second session
LAFI
at
Peek-A-Boo
Chair(s):
Atılım Güneş Baydin
University of Oxford
11:00
40m
Talk
Invited talk: TORAX - A Fast and Differentiable Tokamak Transport Simulator in JAX (Remote)
LAFI
Jonathan Citrin
Google Deepmind
11:41
15m
Talk
Data-Parallel Differentiation by Optic Composition
LAFI
Paul Wilson
University of Southampton
Fabio Zanasi
University College London
11:57
15m
Talk
Data-oriented Design for Differentiable, Probabilistic Programming (Remote)
LAFI
Owen Lynch
University of Oxford
Maria-Nicoleta Craciun
University of Oxford
Younesse Kaddar
University of Oxford
Sam Staton
University of Oxford
12:13
15m
Talk
A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo)
LAFI
Kartik Chandra
MIT
Tony Chen
MIT
Joshua B. Tenenbaum
Massachusetts Institute of Technology
Jonathan Ragan-Kelley
Massachusetts Institute of Technology
12:30 - 14:00
Lunch
Catering
at
Four Square Ballroom
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:30
Backends and Teaching
Dafny
at
Hopscotch
Chair(s):
Stefan Zetzsche
Amazon Web Services
14:00
18m
Talk
Baking for Dafny: A CakeML Backend for Dafny
Dafny
Daniel Nezamabadi
Chalmers University of Technology and University of Gothenburg
Magnus O. Myreen
Chalmers University of Technology
Pre-print
14:18
18m
Talk
Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
Dafny
Wojciech Różowski
University College London
Georges-Axel Jaloyan
Amazon Web Services
Sean McLaughlin
Amazon Web Services
14:36
18m
Talk
Performant, Readable and Interoperable Rust from Dafny
Dafny
Mikael Mayer
Automated Reasoning Group, Amazon Web Services
Shadaj Laddad
University of California at Berkeley
Fabio Madge
Automated Reasoning Group, Amazon Web Services
Siva Somayyajula
Amazon Web Services
Jean-Baptiste Tristan
Amazon Web Services
14:54
18m
Talk
Randomised Testing of the Dafny Compiler: Into the CI
Dafny
Karnbongkot Boonriong
Imperial College London
Alastair F. Donaldson
Imperial College London
Stefan Zetzsche
Amazon Web Services
15:12
18m
Talk
Teaching Types and Non-Interference in Dafny
Dafny
Bryan Parno
Carnegie Mellon University
14:00 - 15:30
MPL: Provably Efficient Parallel Programming
Tutorials
at
Patty Cake
14:00
90m
Tutorial
MPL: Provably Efficient Parallel Programming
Tutorials
P:
Sam Westrick
New York University
Link to publication
14:00 - 15:30
Third session
LAFI
at
Peek-A-Boo
Chair(s):
Matthijs Vákár
Utrecht University
14:00
40m
Talk
Invited talk: Modern Bayesian Experimental Design
LAFI
Desi R. Ivavona
University of Oxford
14:41
15m
Talk
Semantics of the memo Probabilistic Programming Language
LAFI
Kartik Chandra
MIT
Nada Amin
Harvard University
Yizhou Zhang
University of Waterloo
14:57
15m
Talk
NP-NUTS: A Nonparametric No-U-Turn Sampler
LAFI
Maria-Nicoleta Craciun
University of Oxford
C.-H. Luke Ong
NTU
Sam Staton
University of Oxford
Matthijs Vákár
Utrecht University
File Attached
15:13
15m
Talk
Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote)
LAFI
Daniel Goodman
Oracle Labs
Adam Pocock
Oracle Labs
Natalia Kosilova
Oracle Labs
File Attached
15:30 - 16:00
Break
Catering
at
Breakroom
15:30
30m
Coffee break
Break
Catering
16:00 - 18:00
Verified Code Synthesis
Dafny
at
Hopscotch
Chair(s):
Stefan Zetzsche
Amazon Web Services
16:00
18m
Talk
Laurel: Unblocking Automated Verification with Large Language Models
Dafny
Eric Mugnier
University of California San Diego
Emmanuel Anaya Gonzalez
UCSD
Nadia Polikarpova
University of California at San Diego
Ranjit Jhala
University of California at San Diego
Zhou Yuanyuan
UCSD
16:18
18m
Talk
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Dafny
David Brandfonbrener
Harvard
Simon Henniger
Technical University of Munich
Sibi Raja
Harvard
Tarun Prasad
Harvard
Chloe Loughridge
Harvard University
Federico Cassano
Northeastern University
Sabrina Ruixin Hu
Harvard
Jianang Yang
Million.js
William E. Byrd
University of Alabama at Birmingham, USA
Robert Zinkov
University of Oxford
Nada Amin
Harvard University
16:36
18m
Talk
dafny-annotator: AI-Assisted Verification of Dafny Programs
Dafny
Gabriel Poesia
Stanford University
Chloe Loughridge
Harvard University
Nada Amin
Harvard University
16:54
18m
Talk
Dafny as Verification-Aware Intermediate Language for Code Generation
Dafny
Yue Chen Li
Massachusetts Institute of Technology
Stefan Zetzsche
Amazon Web Services
Siva Somayyajula
Amazon Web Services
Pre-print
17:12
18m
Talk
DafnyBench: A Benchmark for Formal Software Verification
Dafny
Chloe Loughridge
Harvard University
Qinyi Sun
Massachusetts Institute of Technology
Seth Ahrenbach
Beneficial AI Foundation
Federico Cassano
Northeastern University
Chuyue Sun
Stanford University
Ying Sheng
Stanford University
Anish Mudide
Massachusetts Institute of Technology
Md Rakib Hossain Misu
University of California Irvine
Nada Amin
Harvard University
Max Tegmark
Massachusetts Institute of Technology
17:30
18m
Talk
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Dafny
Saikat Chakraborty
Microsoft Research
Gabriel Ebner
Microsoft Research
Siddharth Bhat
University of Cambridge
Sarah Fakhoury
Microsoft Research
Sakina Fatima
University of Ottawa
Shuvendu K. Lahiri
Microsoft Research
Nikhil Swamy
Microsoft Research
17:48
12m
Day closing
Day closing
Dafny
Stefan Zetzsche
Amazon Web Services
16:00 - 17:30
MPL: Provably Efficient Parallel Programming
Tutorials
at
Patty Cake
16:00
90m
Tutorial
MPL: Provably Efficient Parallel Programming
Tutorials
P:
Sam Westrick
New York University
Link to publication
16:00 - 17:30
Fourth session
LAFI
at
Peek-A-Boo
Chair(s):
Atılım Güneş Baydin
University of Oxford
16:00
15m
Talk
Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models (Remote)
LAFI
Christian Weilbach
University of British Columbia
Frank Wood
University of Oxford
16:16
15m
Talk
State Space Model Programming in Turing.jl
LAFI
Tim Hargreaves
Department of Engineering, University of Cambridge
Qing Li
Department of Engineering, University of Cambridge
Charles Knipp
Federal Reserve Board of Governors, USA
Frederic Wantiez
Simon J. Godsill
Department of Engineering, University of Cambridge
Hong Ge
University of Cambridge
File Attached
16:32
55m
Other
Poster session
LAFI
17:28
2m
Day closing
Closing remarks
LAFI
Atılım Güneş Baydin
University of Oxford
Mon 20 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Session 1
WAW
at
Dodgeball
09:00
40m
Keynote
Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox
WAW
Chris Fallin
F5
09:40
25m
Talk
An MLIR Dialect for WebAssembly
WAW
Byeongjee Kang
Carnegie Mellon University
Harsh Desai
Carnegie Mellon University
Limin Jia
Carnegie Mellon University
Brandon Lucia
Carnegie Mellon University, USA
10:05
25m
Talk
Meta-tracing Interpreters in WebAssembly
WAW
Andrew Brown
Portland State University
Andrew Tolmach
Portland State University
09:00 - 10:30
Session 1
PADL
at
Duck, Duck Goose
Chair(s):
German Vidal
Universitat Politecnica de Valencia
09:00
60m
Keynote
Invited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance and agreement
PADL
Y. Annie Liu
Stony Brook University
File Attached
10:00
30m
Talk
Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
Best Student Paper –Honorable Mention
PADL
Kento Takyu
Waseda University
Kazunori Ueda
Waseda University
File Attached
09:00 - 10:30
Keynote Talk and Cyber-Physical Systems
VMCAI
at
Hopscotch
Chair(s):
Sriram Sankaranarayanan
University of Colorado, Boulder
09:00
60m
Talk
Keynote Talk: Formal methods in a model-free, data-driven world
VMCAI
Jyotirmoy Deshmukh
University of Southern California
10:00
30m
Talk
Synthesis of Controllers for Continuous Blackbox Systems
VMCAI
Benedikt Maderbacher
Graz University of Technology
Felix Windisch
Graz University of Technology
Alberto Larrauri
University of Oxford
Roderick Bloem
Institute of Software Technology, Graz University of Technology
09:00 - 10:30
Session 1
PriSC
at
Jax
09:00
4m
Day opening
Opening Remarks
PriSC
Marco Patrignani
University of Trento
Marco Vassena
Utrecht University
09:05
59m
Keynote
Keynote: Bringing Verified Cryptographic Protocols to Practice
PriSC
Bryan Parno
Carnegie Mellon University
10:05
25m
Talk
A Semantic Approach to Robust Property Preservation
PriSC
Niklas Mück
MPI-SWS
Michael Sammler
Institute of Science and Technology Austria
Aina Linn Georges
Max Planck Institute for Software Systems (MPI-SWS)
Derek Dreyer
MPI-SWS
Deepak Garg
MPI-SWS
09:00 - 10:30
Session 1
CPP
at
Marco Polo
Chair(s):
Nicolas Tabareau
Inria
09:00
60m
Keynote
Prospects for Computer Formalization of Infinite-Dimensional Category Theory
CPP
Emily Riehl
Johns Hopkins University
10:00
30m
Talk
Certifying rings of integers in number fields
distinguished paper
remote presentation
CPP
Anne Baanen
Vrije Universiteit Amsterdam
Alain Chavarri Villarello
Vrije Universiteit Amsterdam
Sander R. Dahmen
Vrije Universiteit Amsterdam
09:00 - 10:30
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
at
Red Rover
09:00
90m
Tutorial
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
P:
Peter Müller
ETH Zurich
P:
Thibault Dardinier
ETH Zurich
10:30 - 11:00
Break
Catering
at
Breakroom
10:30
30m
Coffee break
Break
Catering
11:00 - 12:30
Session 2
WAW
at
Dodgeball
11:00
40m
Keynote
Adventures in Making Wasm Fast and More Secure
WAW
Shravan Ravi Narayan
11:40
25m
Talk
A Coq Formalization of WebAssembly Execution Costs
WAW
John Shortt
University of Ottawa
12:05
25m
Talk
The WebAssembly Component Model
WAW
Lucy Menon
Microsoft
Luke Wagner
Fastly
11:00 - 12:30
Session 2
PADL
at
Duck, Duck Goose
Chair(s):
Michael Hanus
Kiel University
11:00
30m
Talk
Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System
PADL
Jim Newton
EPITA / LRE https://www.lre.epita.fr
11:30
30m
Talk
Haskell Based Spreadsheets
PADL
Ignacio Ballesteros
IMDEA Software Institute and Universidad Politécnica de Madrid
Luis Eduardo Bueso de Barrio
Universidad Politécnica de Madrid
Julio Mariño
Universidad Politécnica de Madrid
File Attached
12:00
30m
Talk
The Scenic Route to Deforestation
PADL
Steven Libby
Vincent Robinson
University of Portland
11:00 - 12:30
Abstract Interpretation # 1
VMCAI
at
Hopscotch
Chair(s):
Kedar Namjoshi
Nokia Bell Labs
11:00
30m
Talk
Affine Disjunctive Invariant Generation with Farkas’ Lemma
VMCAI
Jingyu Ke
Shanghai Jiao Tong University
Hongfei Fu
Shanghai Jiao Tong University
Hongming Liu
Shanghai Jiao Tong University
Zhouyue Sun
Shanghai Jiao Tong University
Liqian Chen
National University of Defense Technology
Guoqiang Li
Shanghai Jiao Tong University
11:30
30m
Talk
Automatic Inference of Relational Object Invariants
VMCAI
Yusen Su
University of Waterloo
Jorge A. Navas
Certora
Arie Gurfinkel
University of Waterloo
Isabel Garcia-Contreras
University of Waterloo
12:00
30m
Talk
A Static Analysis of Entanglement
VMCAI
Nicola Assolini
University of Verona
Alessandra Di Pierro
University of Verona
Isabella Mastroeni
University of Verona
11:00 - 12:30
Session 2
PriSC
at
Jax
11:00
25m
Talk
ILA: Correctness via Type Checking for Fully Homomorphic Encryption
PriSC
Tarakaram Gollamudi
None
Anitha Gollamudi
University of Massachusetts Lowell
Joshua Gancher
Northeastern University
11:25
24m
Talk
Leveraging Duality for Programming with zkSNARKs
PriSC
Rahul Krishnan
University of Wisconsin-Madison
Ethan Cecchetti
University of Wisconsin-Madison
11:50
24m
Talk
Preservation of Speculative Constant-time by Compilation
PriSC
Santiago Arranz Olmos
Max Planck Institute for Security and Privacy
Gilles Barthe
MPI-SP; IMDEA Software Institute
Lionel Blatter
Max Planck Institute for Security and Privacy
Benjamin Gregoire
INRIA
Vincent Laporte
Inria
11:00 - 12:30
Session 2
CPP
at
Marco Polo
Chair(s):
Jennifer Paykin
Intel
11:00
30m
Talk
Split Decisions: Explicit Contexts for Substructural Languages
distinguished paper
CPP
Daniel Zackon
McGill University
Chuta Sano
McGill University
Alberto Momigliano
Università degli Studi di Milano
Brigitte Pientka
McGill University
Link to publication
DOI
11:30
30m
Talk
Machine Checked Proofs and Programs in Algebraic Combinatorics
CPP
Florent Hivert
Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA
12:00
30m
Talk
Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
remote presentation
CPP
Nicolas Chappe
Inria Lyon, LIP
Ludovic Henrio
University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP
Yannick Zakowski
Inria
11:00 - 12:30
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
at
Red Rover
11:00
90m
Tutorial
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
P:
Peter Müller
ETH Zurich
P:
Thibault Dardinier
ETH Zurich
12:30 - 14:00
Lunch
Catering
at
Four Square Ballroom
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:30
Session 3
WAW
at
Dodgeball
14:00
40m
Keynote
Beyond the Baseline: Experimental WebAssembly for High Performance
WAW
Deepti Gandluri
Google
14:40
25m
Talk
Continuing Stack Switching in Wasmtime
remote
WAW
Frank Emrich
University of Edinburgh, UK
Daniel Hillerström
Category Labs and The University of Edinburgh
Link to publication
Pre-print
15:05
25m
Talk
Experience Report: Stack Switching in Wasm SpecTec
WAW
Yalun Liang
Shanghai Jiao Tong University
Sam Lindley
The University of Edinburgh
Andreas Rossberg
Independent
14:00 - 15:30
Session 3
PADL
at
Duck, Duck Goose
Chair(s):
Kazunori Ueda
Waseda University
14:00
30m
Talk
A practical approach to handling tabular data in logic
PADL
Robin De Vogelaere
KU Leuven
Kylian Van Dessel
Leuven.AI, Belgium
Joost Vennekens
KU Leuven
14:30
30m
Talk
C3G: Causally Constrained Counterfactual Generation
PADL
Sopam Dasgupta
Farhad Shakerin
Microsoft
Joaquín Arias
Universidad Rey Juan Carlos
Elmer Salazar
The University of Texas at Dallas
Gopal Gupta
15:00
30m
Talk
On Bridging Prolog and Python to Enhance an Inductive Logic Programming System
PADL
Vitor Santos Costa
University of Porto, Portugal
Miguel Areias
University of Porto, Portugal
14:00 - 15:30
Model Checking
VMCAI
at
Hopscotch
Chair(s):
Arie Gurfinkel
University of Waterloo
14:00
30m
Talk
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
VMCAI
Florian Bruse
University of Kassel
14:30
30m
Talk
Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
VMCAI
Paul Eichler
CISPA - Helmholtz Center for Information Security
Swen Jacobs
CISPA
Chana Weil-Kennedy
IMDEA Software Institute
15:00
30m
Talk
Property-agnostic base case extension for scalable verification of distributed systems
VMCAI
Kyle Storey
Brigham Young University
Eric Mercer
Brigham Young University
14:00 - 15:30
Session 3
PriSC
at
Jax
14:00
24m
Talk
Auditing Rust Crates Effectively
PriSC
Lydia Zoghbi
University of California, San Diego
David Thien
University of California, San Diego
Ranjit Jhala
UCSD
Deian Stefan
University of California at San Diego
Caleb Stanford
University of California, Davis
14:25
24m
Talk
Automatic Inference of Enclave Placement in LLVM Compiler
PriSC
Wesley B Nuzzo
University of Massachusetts, Lowell (UML)
Mohamed Elwakil
U.S. Coast Guard Academy
Anitha Gollamudi
University of Massachusetts Lowell
14:50
24m
Talk
Counterexamples in Safe Rust
PriSC
Muhammad Hassnain
University of California, Davis
Caleb Stanford
University of California, Davis
14:00 - 15:30
Session 3
CPP
at
Marco Polo
Chair(s):
Yasuhiko Minamide
Tokyo Institute of Technology
14:00
30m
Talk
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
CPP
Dohan Kim
University of Innsbruck
Teppei Saito
Japan Advanced Institute of Science and Technology, Japan
René Thiemann
University of Innsbruck
Akihisa Yamada
National Institute of Informatics
14:30
30m
Talk
Intrinsically Correct Sorting in Cubical Agda
CPP
Cass Alexandru
RPTU Kaiserslautern-Landau
Vikraman Choudhury
Università di Bologna & Inria OLAS
Jurriaan Rot
Radboud University Nijmegen
Niels van der Weide
Radboud University
15:00
30m
Talk
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
CPP
Christina Kirk
University of Innsbruck
Aart Middeldorp
University of Innsbruck
14:00 - 15:30
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tutorials
at
Red Rover
14:00
90m
Tutorial
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tutorials
P:
Oded Padon
Weizmann Institute of Science
15:30 - 16:00
Break
Catering
at
Breakroom
15:30
30m
Coffee break
Break
Catering
16:00 - 17:30
Session 4
WAW
at
Dodgeball
16:00
25m
Talk
A Transactions Extension for Web Assembly
remote
WAW
Eliot Moss
University of Massachusetts at Amherst
16:25
25m
Talk
A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
WAW
Guannan Wei
Inria/ENS; Tufts University
Alexander Bai
MPI-SWS
Dinghong Zhong
Xi'an Jiaotong University
Jiatai Zhang
Tufts University
16:50
40m
Talk
Lighting talks and closing discussion
WAW
Conrad Watt
Nanyang Technological University
16:00 - 17:30
Session 4
PADL
at
Duck, Duck Goose
Chair(s):
Vitor Santos Costa
University of Porto, Portugal
16:00
30m
Talk
MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
PADL
Felipe Gorostiaga
IMDEA Software Institute
Martin Ceresa
IMDEA Software Institute
César Sánchez
IMDEA Software Institute
16:30
30m
Talk
Checking Concurrency Coding Rules
PADL
Lars-Åke Fredlund
Universidad Politécnica de Madrid
Ángel Herranz
Universidad Politécnica de Madrid
Julio Mariño
Universidad Politécnica de Madrid
17:00
10m
Talk
Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
PADL
Michael Hanus
Kiel University
17:10
10m
Talk
Logic Programming with Extensible Types (Lightning talk)
PADL
Ivan Perez
NASA Ames Research Center
Ángel Herranz
Universidad Politécnica de Madrid
P:
Julio Mariño
Universidad Politécnica de Madrid
16:00 - 17:30
Applications
VMCAI
at
Hopscotch
Chair(s):
Jyotirmoy Deshmukh
University of Southern California
16:00
30m
Talk
ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
VMCAI
Gustav S. Bruhns
Aalborg University
Martin P. Hansen
Aalborg University
Rasmus Hebsgaard
Aalborg University
Frederik M. W. Hyldgaard
Aalborg University
Jiri Srba
Aalborg University
16:30
30m
Talk
Constructing Trustworthy Smart Contracts
VMCAI
Devora Chait-Roth
New York University
Kedar Namjoshi
Nokia Bell Labs
17:00
30m
Talk
Automated Flaw Detection for Industrial Robot RESTful Service
Recorded
VMCAI
Yuncheng Wang
Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China
Puzhuo Liu
Tsinghua University
Yaowen Zheng
Institute of Information Engineering at Chinese Academy of Sciences
Dongliang Fang
Beijing Key Laboratory of IOT Information Security Technology, Institute of Information Engineering, CAS, China; School of Cyber Security, University of Chinese Academy of Sciences, China
Zhiwen Pan
Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China
Shuaizong Si
Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China
Weidong Zhang
Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, China
Limin Sun
Institute of Information Engineering at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Media Attached
16:00 - 17:30
Session 4
PriSC
at
Jax
16:00
24m
Talk
BeePL: Correct-by-compilation kernel extensions
PriSC
Swarn Priya
Virginia Tech
Tim Steenvoorden
Open Universiteit
Connor Sughrue
Virginia Tech
Frédéric Besson
Inria, Rennes
Freek Verbeek
Open Universiteit & Virginia Tech
16:25
24m
Talk
Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
PriSC
Julian Rosemann
Saarland University, Saarland Informatics Campus
Sebastian Hack
Saarland University, Saarland Informatics Campus
Deepak Garg
MPI-SWS
File Attached
16:50
24m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
PriSC
Sören van der Wall
TU Braunschweig
Roland Meyer
TU Braunschweig
Link to publication
DOI
17:15
15m
Day closing
Closing Remarks
PriSC
Marco Patrignani
University of Trento
Marco Vassena
Utrecht University
16:00 - 17:30
Session 4
CPP
at
Marco Polo
Chair(s):
Brigitte Pientka
McGill University
16:00
30m
Talk
Formalized Burrows-Wheeler Transform
CPP
Louis Cheung
University of Melbourne
Alistair Moffat
The University of Melbourne
Christine Rizkallah
University of Melbourne
16:30
30m
Talk
Verified and Efficient Matching of Regular Expressions with Lookaround
remote presentation
CPP
Agnishom Chattopadhyay
Imiron
Angela W. Li
Rice University
Konstantinos Mamouras
Rice University
17:00
30m
Talk
Further Tackling Post Correspondence Problem and Proof Generation
CPP
Akihiro Omori
Department of Mathematical and Computing Science, Tokyo Institute of Technology
Yasuhiko Minamide
Tokyo Institute of Technology
16:00 - 17:30
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tutorials
at
Red Rover
16:00
90m
Tutorial
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tutorials
P:
Oded Padon
Weizmann Institute of Science
Tue 21 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Keynote Talk (Tuesday) and Learning
VMCAI
at
Hopscotch
Chair(s):
Ashutosh Trivedi
University of Colorado Boulder
09:00
60m
Talk
Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic program analysis
VMCAI
Alexandra Silva
Cornell University
10:00
30m
Talk
1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
VMCAI
Muqsit Azeem
Technical University of Munich
Debraj Chakraborty
Masaryk University
Sudeep Kanav
LMU Munich
Jan Kretinsky
Masaryk University, Czech Republic
Mohammadsadegh Mohagheghi
Masaryk University
Stefanie Mohr
Technical University of Munich
Maximilian Weininger
Institute of Science and Technology Austria
09:00 - 10:30
Session 5
PADL
at
Keep Away
Chair(s):
Esra Erdem
Sabanci University
09:00
60m
Keynote
Invited Talk: Bridging Safety and Performance
PADL
Umut A. Acar
Carnegie Mellon University
10:00
30m
Talk
SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
Best student paper
PADL
Zachary Hansen
University of Nebraska Omaha
Yuliya Lierler
University of Nebraska
09:00 - 10:30
Session 5
CPP
at
Marco Polo
Chair(s):
Sandrine Blazy
University of Rennes
09:00
60m
Keynote
CRIS: The power of imagination in specification and verification
CPP
A:
Chung-Kil Hur
Seoul National University
10:00
30m
Talk
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
distinguished paper
CPP
Simon Friis Vindum
Aarhus University
Aina Linn Georges
Max Planck Institute for Software Systems (MPI-SWS)
Lars Birkedal
Aarhus University
09:00 - 10:30
Stateless model checking concurrent and distributed programs
Tutorials
at
Paper
09:00
90m
Tutorial
Stateless Model Checking Concurrent and Distributed Programs
Tutorials
P:
Michalis Kokologiannakis
ETH Zurich
P:
Viktor Vafeiadis
MPI-SWS
09:00 - 10:30
Introduction and Keynote
TPSA
at
Patty Cake
09:00
10m
Day opening
Introduction
TPSA
Noam Zilberstein
Cornell University
Azalea Raad
Imperial College London
Jules Villard
Meta
09:10
60m
Keynote
Improving Static Analysis using Information Collected at Runtime
Keynote
TPSA
Radu Grigore
Meta
09:00 - 10:30
First Session
PLMW @ POPL
at
Peek-A-Boo
Chair(s):
Leonidas Lampropoulos
University of Maryland, College Park
09:00
45m
Talk
Getting the Most Out of POPL
PLMW @ POPL
Joseph W. Cutler
University of Pennsylvania
09:45
45m
Social Event
Icebreaker
PLMW @ POPL
Leonidas Lampropoulos
University of Maryland, College Park
09:00 - 10:30
High-level abstraction and automation
PEPM
at
Scissors
Chair(s):
Sam Lindley
The University of Edinburgh
09:00
10m
Day opening
Welcome
PEPM
Y. Annie Liu
Stony Brook University
09:10
50m
Keynote
The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract)
PEPM
Satnam Singh
Groq
DOI
10:00
30m
Research paper
A Type Safe Calculus for Generating Syntax-Directed Editors
Remote
PEPM
Andreas Tor Mortensen
Department of Computer Science, Aalborg University
Benjamin Bennetzen
Department of Computer Science, Aalborg University
Nikolaj Rossander Kristensen
Department of Computer Science, Aalborg University
Peter Buus Steffensen
Department of Computer Science, Aalborg University
Hans Hüttel
Department of Computer Science, Aalborg University
Sune Skaanning Engtorp
Department of Computer Science, University of Copenhagen
DOI
10:30 - 11:00
Break
Catering
at
Breakroom
10:30
30m
Coffee break
Break
Catering
11:00 - 12:30
Verification
VMCAI
at
Hopscotch
Chair(s):
Isabella Mastroeni
University of Verona
11:00
30m
Talk
A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
VMCAI
Daisuke Ishii
JAIST
11:30
30m
Talk
Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
VMCAI
Mario Bucev
EPFL
Samuel Chassot
EPFL, LARA
Simon Felix
Ateleris GmbH
Filip Schramka
Ateleris GmbH
Viktor Kunčak
EPFL, Switzerland
Pre-print
12:00
30m
Talk
Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training
VMCAI
Junfeng Yang
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University
Junfeng Yang
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University
Xin Chen
University of New Mexico, USA
Qin Li
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University
11:00 - 12:30
Session 6
PADL
at
Keep Away
Chair(s):
Fang Li
Oklahoma Christian University
11:00
30m
Talk
ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
PADL
Daniela Inclezan
Miami University, USA
Hunter Lockwood
Myaamia Center & Miami University
Anita Baral
Miami University
Jitendra Sharma
Miami University
Pratiksha Shrestha
Miami University
11:30
30m
Talk
A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
PADL
Yan Yan
Southeast University, Nanjing
Junru Li
Southeast University, Nanjing
Fangzhou Liu
Southeast University, Nanjing
Zerong Wang
Southeast University, Nanjing
Zhizheng Zhang
Southeast University, Nanjing
12:00
30m
Talk
Automated Playing of Survival Video Games with Commonsense Reasoning (short paper)
PADL
Dan Nguyen
University of Texas at Dallas, USA
Bryant Hargreaves
University of Texas at Dallas, USA
Keegan Kimbrell
University of Texas at Dallas, USA
Gopal Gupta
11:00 - 12:30
Session 6
CPP
at
Marco Polo
Chair(s):
Kathrin Stark
Heriot-Watt University
11:00
30m
Talk
Leakage-Free Probabilistic Jasmin Programs
CPP
Denis Firsov
Tallinn University of Technology
Tiago Oliveira
SandboxAQ
José Bacelar Almeira
University of Minho & INESC TEC
Dominique Unruh
RWTH Aachen
11:30
30m
Talk
Formally verified hardening of C programs against hardware fault injection
CPP
Basile Pesin
Ecole Nationale de l'Aviation Civile (ENAC)
Sylvain Boulmé
Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
David Monniaux
CNRS
Marie-Laure Potet
Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG
Pre-print
12:00
30m
Talk
CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
remote presentation
CPP
Wolfgang Meier
Aarhus University
Martin Jensen
Aarhus University
Jean Pichon-Pharabod
Aarhus University
Bas Spitters
Aarhus University
Pre-print
11:00 - 12:30
Stateless model checking concurrent and distributed programs
Tutorials
at
Paper
11:00
90m
Tutorial
Stateless Model Checking Concurrent and Distributed Programs
Tutorials
P:
Michalis Kokologiannakis
ETH Zurich
P:
Viktor Vafeiadis
MPI-SWS
11:00 - 12:30
Program Logics
TPSA
at
Patty Cake
11:00
18m
Talk
Data Structure Abstraction and Incorrectness Separation Logic
TPSA
Andreas Lööw
Imperial College London
11:18
18m
Talk
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
TPSA
Conrad Zimmerman
Northeastern University
Jenna DiVincenzo (Wise)
Purdue University
Pre-print
11:36
18m
Talk
Partial Incorrectness Logic
TPSA
Lena Verscht
RWTH Aachen University; Saarland University
Ānrán Wáng
Saarland University
Benjamin Lucien Kaminski
Saarland University; University College London
11:54
18m
Talk
Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching
TPSA
James Li
Cornell University
Noam Zilberstein
Cornell University
Alexandra Silva
Cornell University
12:12
18m
Talk
U-turn: Forward-driven backward analysis for incorrectness
TPSA
Flavio Ascari
University of Pisa
Roberto Bruni
University of Pisa
Roberta Gori
Diaprtimento di Informatica, Universita' di Pisa, Italy
Azalea Raad
Imperial College London
11:00 - 12:30
Second Session
PLMW @ POPL
at
Peek-A-Boo
Chair(s):
Bor-Yuh Evan Chang
University of Colorado Boulder & Amazon
11:00
45m
Talk
How to give a good talk
PLMW @ POPL
Michael Greenberg
Stevens Institute of Technology
11:45
45m
Talk
My Journey in Secure Compilation
PLMW @ POPL
Cătălin Hriţcu
MPI-SP
Pre-print
11:00 - 12:30
Language design, pedagogical tool, and staged interpreter
PEPM
at
Scissors
Chair(s):
Michael Hanus
Kiel University
11:00
45m
Keynote
The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk)
PEPM
William J. Bowman
University of British Columbia
DOI
Pre-print
File Attached
11:45
30m
Research paper
Algebraic Stepper for Simple Modules
PEPM
Kenichi Asai
Ochanomizu University
Hinano Akiyama
Ochanomizu University
DOI
12:15
15m
Short-paper
Collapsing Towers for Side-Channel Security (Short Paper)
PEPM
Cameron Wong
Harvard SEAS
Muhammad Abdullah
MIT
Yuheng Yang
MIT
Mengjia Yan
MIT
Adam Chlipala
Massachusetts Institute of Technology
Nada Amin
Harvard University
File Attached
12:30 - 14:00
Lunch
Catering
at
Four Square Ballroom
12:30
90m
Lunch
Lunch
Catering
12:30 - 14:00
SIGPLAN SC Meeting
Catering
at
Virtual Only
12:30
90m
Meeting
SIGPLAN SC Meeting
Catering
14:00 - 15:30
Abstract Interpretation # 2
VMCAI
at
Hopscotch
Chair(s):
Alexandra Silva
Cornell University
14:00
30m
Talk
Abstract Local Completeness: A Local form of Abstract Non-Interference
VMCAI
Isabella Mastroeni
University of Verona
14:30
30m
Talk
An Abstract Domain for Heap Commutativity
VMCAI
Jared Pincus
Boston University
Eric Koskinen
Stevens Institute of Technology
15:00
30m
Talk
Two-way collaboration between flow and proof in SPARK
VMCAI
Claire Dross
AdaCore
Joffrey Huguet
AdaCore
Johannes Kanig
AdaCore
14:00 - 15:30
Session 7
PADL
at
Keep Away
Chair(s):
Daniela Inclezan
Miami University
14:00
30m
Talk
Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
PADL
Fang Li
Oklahoma Christian University
Fei Zuo
University of Central Oklahoma
Gopal Gupta
14:30
30m
Talk
Leveraging LLM Reasoning with Dual Horn Programs
RECORDED
PADL
Paul Tarau
University of North Texas
15:00
30m
Talk
Enhancing network diagnosis with reflection in Prolog (extended abstract)
RECORDED
PADL
Anduo Wang
Temple University, USA
Pre-print
14:00 - 15:30
Session 7
CPP
at
Marco Polo
Chair(s):
Mario Carneiro
CMU
14:00
30m
Talk
Nominal Matching Logic With Fixpoints
CPP
James Cheney
University of Edinburgh
Maribel Fernandez
King's College London
Mircea Sebe
UIUC
14:30
30m
Talk
Tactic Script Optimisation for Aesop
CPP
Jannis Limperg
University of Munich (LMU)
Link to publication
DOI
15:00
30m
Talk
An Isabelle/HOL Framework for Synthetic Completeness Proofs
remote presentation
CPP
Asta Halkjær From
University of Copenhagen
DOI
14:00 - 15:30
Static Analysis and Abstract Interpretation
TPSA
at
Patty Cake
14:00
18m
Talk
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
Remote
TPSA
Florian Sextl
TU Wien, Austria
Adam Rogalewicz
Brno University of Technology, Czechia
Tomáš Vojnar
Brno University of Technology
Florian Zuleger
TU Vienna
Pre-print
14:18
18m
Talk
Calculational design of Incorrectness Separation Logic
TPSA
Lorenzo Gazzella
Università di Pisa
14:36
18m
Talk
Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation
TPSA
Pedro Carrott
Imperial College London
Sacha-Élie Ayoun
Imperial College London
Azalea Raad
Imperial College London
14:54
18m
Talk
Enhancing Infer Compositional Analysis with Summary Specialization
TPSA
David Pichardie
Meta
15:12
18m
Talk
Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms
TPSA
Christian Fontenot
University of Colorado Boulder
Gowtham Kaki
University of Colorado at Boulder
Bor-Yuh Evan Chang
University of Colorado Boulder & Amazon
14:00 - 15:30
Third Session
PLMW @ POPL
at
Peek-A-Boo
Chair(s):
Andrew K. Hirsch
University at Buffalo, SUNY
14:00
45m
Talk
From operational semantics to verified compilation (and more)
PLMW @ POPL
Sandrine Blazy
University of Rennes
14:45
45m
Talk
A Research Career in Balance
PLMW @ POPL
Andrew Myers
Cornell University
14:00 - 15:30
Types and meta theory
PEPM
at
Scissors
Chair(s):
Kenichi Asai
Ochanomizu University
14:00
45m
Keynote
A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract)
PEPM
Brigitte Pientka
McGill University
DOI
14:45
30m
Research paper
Typed Program Analysis without Encodings
PEPM
Barry Jay
DOI
15:15
15m
Short-paper
A Fuelled Self-Reducer for System T (Short Paper)
PEPM
Greg Brown
University of Edinburgh
File Attached
15:30 - 16:00
Break
Catering
at
Breakroom
15:30
30m
Coffee break
Break
Catering
16:00 - 17:30
Concurrency
VMCAI
at
Hopscotch
Chair(s):
Sriram Sankaranarayanan
University of Colorado, Boulder
16:00
30m
Talk
LLOR: Automated Repair of OpenMP Programs
VMCAI
Gautam Muduganti
Indian Institute of Technology Hyderabad, India
Utpal Bora
University of Cambridge
Saurabh Joshi
Supra Research
Ramakrishna Upadrasta
16:30
30m
Talk
Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
VMCAI
Ruoxi Zhang
University of Waterloo
Richard Trefler
University of Waterloo, Canada
Kedar Namjoshi
Nokia Bell Labs
17:00
30m
Talk
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
VMCAI
Julian Erhard
LMU Munich; TU Munich
Manuel Bentele
University of Freiburg
Matthias Heizmann
University of Freiburg, Germany
Dominik Klumpp
University of Freiburg
Simmo Saan
University of Tartu, Estonia
Frank Schüssele
University of Freiburg
Michael Schwarz
TU Munich
Helmut Seidl
TU Munich
Sarah Tilscher
Technical University of Munich, Garching, Germany
Vesal Vojdani
University of Tartu
Pre-print
16:00 - 17:30
Session 8
CPP
at
Marco Polo
Chair(s):
Lars Birkedal
Aarhus University
16:00
30m
Talk
Formalization of Differential Privacy in Isabelle/HOL
CPP
Tetsuya Sato
Tokyo Institute of Technology
Yasuhiko Minamide
Tokyo Institute of Technology
16:30
30m
Talk
A CHERI C Memory Model for Verified Temporal Safety
CPP
Vadim Zaliva
University of Cambridge, UK
Kayvan Memarian
University of Cambridge
Brian Campbell
University of Edinburgh
Ricardo Almeida
University of Edinburgh
Nathaniel Filardo
University of Cambridge
Ian Stark
The University of Edinburgh
Peter Sewell
University of Cambridge
17:00
30m
Talk
Formalizing the One-way to Hiding Theorem
CPP
Katharina Heidler
Technical University Munich
Dominique Unruh
RWTH Aachen
16:00 - 17:30
Analysis Techniques
TPSA
at
Patty Cake
16:00
18m
Talk
Distributed transactions over mergeable types: A meta-theory for 5G control-plane protocol verification
TPSA
Prasanth Prahladan
University of Colorado Boulder
16:18
18m
Talk
Domain Reasoning In TopKAT: Reduction and Completeness
TPSA
Cheng Zhang
University College London (UCL)
Arthur Azevedo de Amorim
Rochester Institute of Technology, USA
Marco Gaboardi
Boston University
16:36
18m
Talk
From Traces to Program Incorrectness: A Type-Theoretic Approach
TPSA
Yongwei Yuan
Purdue University
Zhe Zhou
Purdue University
Julia Belyakova
Purdue University
Benjamin Delaware
Purdue University
Suresh Jagannathan
Purdue University
Pre-print
16:54
18m
Talk
Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
TPSA
Naifeng Zhang
Carnegie Mellon University
Sanil Rao
Carnegie Mellon University
Mike Franusich
SpiralGen, Inc.
Franz Franchetti
Carnegie Mellon University, USA
17:12
18m
Talk
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
TPSA
Yusuke Matsushita
Kyoto University
Kengo Hirata
University of Edinburgh
Ryo Wakizaka
Kyoto University
16:00 - 17:30
Fourth Session
PLMW @ POPL
at
Peek-A-Boo
Chair(s):
Leonidas Lampropoulos
University of Maryland, College Park
16:00
45m
Talk
How to Write Papers So People Can Read Them
PLMW @ POPL
Derek Dreyer
MPI-SWS
16:45
45m
Panel
PLMW Panel
PLMW @ POPL
Ronald Garcia
University of British Columbia
Mike Dodds
Galois, Inc
Alexandre Moine
New York University
Jenna DiVincenzo (Wise)
Purdue University
16:00 - 17:30
Macros, lenses, and LLMs
PEPM
at
Scissors
Chair(s):
Y. Annie Liu
Stony Brook University
16:00
15m
Short-paper
Type-Sensitive Algebraic Macros (Short Paper)
Remote
PEPM
April Gonçalves
University of Strathclyde
Robert Atkey
University of Strathclyde
File Attached
16:15
30m
Research paper
Characterizations of Partial Well-Behaved Lenses
PEPM
Keishi HASHIBA
The University of Osaka
Keisuke Nakano
Tohoku University
Kazuyuki Asada
Tohoku University
Kentaro Kikuchi
Tohoku University
DOI
16:45
40m
Panel
Semantics-based program manipulation in the age of LLMs
PEPM
William J. Bowman
University of British Columbia
Brigitte Pientka
McGill University
Satnam Singh
Groq
Sam Lindley
The University of Edinburgh
17:25
5m
Day closing
Farewell
PEPM
Y. Annie Liu
Stony Brook University
17:30 - 18:00
Business meeting
CPP
at
Marco Polo
17:30
30m
Meeting
Business Meeting
CPP
Sandrine Blazy
University of Rennes
Nicolas Tabareau
Inria
18:00 - 22:00
Jane Street Social Event
POPL
at
Patty Cake
Chair(s):
Chris Casinghino
Jane Street
Richard A. Eisenberg
Jane Street
18:00
4h
Social Event
Jane Street Game Night
POPL
Richard A. Eisenberg
Jane Street
Chris Casinghino
Jane Street
19:30 - 22:00
POPL PC and SC Dinner
Catering
at
Panzano Restaurant
Wed 22 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
08:55 - 09:00
Welome from the general chair
POPL
at
Marco Polo
08:55
5m
Day opening
Welome from the general chair
POPL
09:00 - 10:00
Keynote
POPL
at
Marco Polo
09:00
60m
Keynote
Finding Good Programs by Avoiding Bad Ones
POPL
Loris D'Antoni
University of California, San Diego
10:00 - 10:40
Break
Catering
at
Breakroom
10:00
40m
Coffee break
Break
Catering
10:40 - 12:00
Automata and Temporal Properties
POPL
at
Marco Polo
Chair(s):
Thomas Ball
Microsoft Research
10:40
20m
Talk
Coinductive Proofs for Temporal Hyperliveness
POPL
Arthur Correnson
CISPA Helmholtz Center for Information Security
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security
Link to publication
DOI
11:00
20m
Talk
Derivative-Guided Symbolic Execution
POPL
Yongwei Yuan
Purdue University
Zhe Zhou
Purdue University
Julia Belyakova
Purdue University
Suresh Jagannathan
Purdue University
11:20
20m
Talk
Symbolic Automata: omega-Regularity Modulo Theories
POPL
Margus Veanes
Microsoft Research
Thomas Ball
Microsoft Research
Gabriel Ebner
Microsoft Research
Ekaterina Zhuchko
Tallinn University of Technology
11:40
20m
Talk
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
POPL
Philippe Heim
CISPA Helmholtz Center for Information Security
Rayna Dimitrova
CISPA Helmholtz Center for Information Security
Pre-print
10:40 - 12:00
Program Analysis
POPL
at
Peek-A-Boo
Chair(s):
Roland Leißa
University of Mannheim, School of Business Informatics and Mathematics
10:40
20m
Talk
Maximal Simplification of Polyhedral Reductions
POPL
Louis Narmour
Colorado State University, University of Rennes, Inria, CNRS, IRISA
Tomofumi Yuki
Sanjay Rajopadhye
Colorado State University
11:00
20m
Talk
Program Analysis via Multiple Context Free Language Reachability
POPL
Giovanna Kobus Conrado
Hong Kong University of Science and Technology
Adam Husted Kjelstrøm
Aarhus University
Jaco van de Pol
Aarhus University
Andreas Pavlogiannis
Aarhus University
11:20
20m
Talk
The Best of Abstract Interpretations
POPL
Roberto Giacobazzi
University of Arizona
Francesco Ranzato
University of Padova
Pre-print
11:40
20m
Talk
An Incremental Algorithm for Algebraic Program Analysis
POPL
Chenyu Zhou
University of Southern California
Yuzhou Fang
University of Southern California
Jingbo Wang
Purdue University
Chao Wang
University of Southern California
12:00 - 13:20
Lunch
Catering
at
Four Square Ballroom
12:00
80m
Lunch
Lunch
Catering
12:00 - 13:20
Mentoring Lunch
Catering
at
Hopscotch
12:00
80m
Lunch
Mentoring Lunch
Catering
12:00 - 13:20
PLMW Steering Committee Lunch
Catering
at
Kick the Can
12:00
80m
Lunch
PLMW Steering Committee Lunch
Catering
13:20 - 14:20
Quantum Computing 1
POPL
at
Marco Polo
Chair(s):
Benjamin Delaware
Purdue University
13:20
20m
Talk
Linear and non-linear relational analyses for Quantum Program Optimization
POPL
Matthew Amy
Simon Fraser University
Joseph Lunderville
Simon Fraser University
13:40
20m
Talk
Automating equational proofs in Dirac notation
Remote
POPL
Yingte Xu
MPI-SP and Institute of Software, Chinese Academy of Sciences
Gilles Barthe
MPI-SP; IMDEA Software Institute
Li Zhou
Institute of Software, Chinese Academy of Sciences
14:00
20m
Talk
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
POPL
Andrea Colledan
University of Bologna & INRIA Sophia Antipolis
Ugo Dal Lago
University of Bologna & INRIA Sophia Antipolis
13:20 - 14:20
Verification 1
POPL
at
Peek-A-Boo
Chair(s):
Julia Belyakova
Purdue University
13:20
20m
Talk
Axe 'Em: Eliminating Spurious States with Induction Axioms
POPL
Neta Elad
Tel Aviv University
Sharon Shoham
Tel Aviv University
Link to publication
DOI
13:40
20m
Talk
A Verified Foreign Function Interface Between Coq and C
POPL
Joomy Korkut
Bloomberg LP
Kathrin Stark
Heriot-Watt University
Andrew W. Appel
Princeton University
14:00
20m
Talk
TensorRight: Automated Verification of Tensor Graph Rewrites
Distinguished Paper
POPL
Jai Arora
University of Illinois at Urbana-Champaign
Sirui Lu
University of Washington
Devansh Jain
University of Illinois at Urbana-Champaign
Tianfan Xu
University of Illinois at Urbana-Champaign
Farzin Houshmand
Google
Phitchaya Mangpo Phothilimthana
Google
Mohsen Lesani
University of California at Santa Cruz
Praveen Narayanan
Google
Karthik Srinivasa Murthy
Google
Rastislav Bodík
Google Research, Brain Team
Amit Sabne
Google
Charith Mendis
University of Illinois at Urbana-Champaign
Link to publication
DOI
14:20 - 15:00
Break
Catering
at
Breakroom
14:20
40m
Coffee break
Break
Catering
15:00 - 16:20
Probabilistic Programming 1
POPL
at
Marco Polo
Chair(s):
Louis Narmour
Colorado State University, University of Rennes, Inria, CNRS, IRISA
15:00
20m
Talk
A quantitative probabilistic relational Hoare logic
POPL
Martin Avanzini
Inria
Gilles Barthe
MPI-SP; IMDEA Software Institute
Benjamin Gregoire
INRIA
Davide Davoli
Université Côte d’Azur, Inria
15:20
20m
Talk
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL
Philipp G. Haselwarter
Aarhus University
Kwing Hei Li
Aarhus University
Alejandro Aguirre
Aarhus University
Simon Oddershede Gregersen
New York University
Joseph Tassarotti
New York University
Lars Birkedal
Aarhus University
Pre-print
15:40
20m
Talk
Compositional imprecise probability: a solution from graded monads and Markov categories
POPL
Jack Liell-Cock
University of Oxford
Sam Staton
University of Oxford
16:00
20m
Talk
Sound and Complete Proof Rules for Probabilistic Termination
POPL
Rupak Majumdar
MPI-SWS
V.R. Sathiyanarayana
MPI-SWS
15:00 - 16:20
Semantic models
POPL
at
Peek-A-Boo
Chair(s):
Vikraman Choudhury
Università di Bologna & Inria OLAS
15:00
20m
Talk
Consistency of a Dependent Calculus of Indistinguishability
POPL
Yiyun Liu
University of Pennsylvania
Jonathan Chan
University of Pennsylvania
Stephanie Weirich
University of Pennsylvania
15:20
20m
Talk
Finite-Choice Logic Programming
POPL
Chris Martens
Northeastern University
Robert Simmons
Independent
Michael Arntzenius
None
Link to publication
DOI
Pre-print
File Attached
15:40
20m
Talk
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
POPL
Eric Giovannini
University of Michigan
Tingting Ding
University of Michigan
Max S. New
University of Michigan
DOI
16:00
20m
Talk
Abstract Operational Methods for Call-by-Push-Value
POPL
Sergey Goncharov
University of Birmingham, School of Comp. Sci.
Stelios Tsampas
FAU Erlangen-Nuremberg, INF 8
Henning Urbat
FAU Erlangen-Nuremberg, INF 8
16:20 - 17:00
Break
Catering
at
Breakroom
16:20
40m
Coffee break
Break
Catering
17:00 - 18:00
TOPLAS
POPL
at
Marco Polo
Chair(s):
Jingbo Wang
Purdue University
17:00
20m
Talk
Universal Composability is Robust Compilation
POPL
Marco Patrignani
University of Trento
Robert Künnemann
CISPA Helmholtz Center for Information Security
Riad S. Wahby
Stanford University, USA
Ethan Cecchetti
University of Wisconsin-Madison
17:20
20m
Talk
Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation
POPL
Roberto Giacobazzi
University of Arizona
Isabella Mastroeni
University of Verona
Elia Perantoni
17:40
20m
Talk
Gradual C0: Symbolic Execution for Gradual Verification
POPL
Jenna DiVincenzo (Wise)
Purdue University
Ian McCormack
Carnegie Mellon University
Hemant Gouni
Carnegie Mellon University, Pittsburgh, Pennsylvania, United States
Jacob Gorenburg
Jan-Paul Ramos-Davila
Cornell University
Mona Zhang
Columbia University
Conrad Zimmerman
Northeastern University
Joshua Sunshine
Carnegie Mellon University
Éric Tanter
University of Chile
Jonathan Aldrich
Carnegie Mellon University
Link to publication
DOI
17:00 - 18:00
Separation Logic
POPL
at
Peek-A-Boo
Chair(s):
Adam Chlipala
Massachusetts Institute of Technology
17:00
20m
Talk
Formal Foundations for Translational Separation Logic Verifiers
POPL
Thibault Dardinier
ETH Zurich
Michael Sammler
Institute of Science and Technology Austria
Gaurav Parthasarathy
ETH Zurich
Alexander J. Summers
University of British Columbia
Peter Müller
ETH Zurich
17:20
20m
Talk
Fulminate: Testing CN Separation-Logic Specifications in C
POPL
Rini Banerjee
University of Cambridge
Kayvan Memarian
University of Cambridge
Dhruv Makwana
University of Cambridge
Christopher Pulte
University of Cambridge
Neel Krishnaswami
University of Cambridge
Peter Sewell
University of Cambridge
DOI
17:40
20m
Talk
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
POPL
Qiyuan Xu
Nanyang Technological University
David Sanan
Singapore Institute of Technology
Zhe Hou
Griffith University
Xiaokun Luan
Peking University
Conrad Watt
Nanyang Technological University
Yang Liu
Nanyang Technological University
18:00 - 20:00
POPL Networking Reception
Catering
at
Four Square Ballroom
18:00
2h
Social Event
POPL Networking Reception
Catering
18:00 - 20:00
SRC Poster Session
Student Research Competition
at
Four Square Corridor
18:00
2h
Poster
Efficient Strong Simulation of High-level Quantum Gates
Student Research Competition
Adam Husted Kjelstrøm
18:00
2h
Poster
Value semantics in reference-based languages
Student Research Competition
Hamza Remmal
EPFL, LAMP
18:00
2h
Poster
Intermittent Concurrency
Student Research Competition
Myra Dotzel
Carnegie Mellon University
Milijana Surbatovich
University of Maryland
Limin Jia
Carnegie Mellon University
18:00
2h
Poster
APIdemic: Verifying Idempotency of REST API Clients
Student Research Competition
Bhavik Kamlesh Goplani
University of Kansas
18:00
2h
Poster
Formalizing Erlang’s Success Typings
Student Research Competition
Elan Semenova
University of Maryland, College Park
Leonidas Lampropoulos
University of Maryland, College Park
18:00
2h
Poster
A Complete Translation from Planning Problems to linear logic
Student Research Competition
Luis Hernan Garcia Paucar
Aston University
Chris Martens
Northeastern University
18:00
2h
Poster
Wanco: WebAssembly AOT Compiler that supports Live Migration
Student Research Competition
Raiki Tamura
Kyoto University
Daisuke Kotani
Kyoto University
Yasuo Okabe
Kyoto University
18:00
2h
Poster
Increasing the Expressiveness of a Gradual Verifier
Student Research Competition
Priyam Gupta
Purdue University
18:00
2h
Poster
M3: A Multi-Stage ML with Mutation
Student Research Competition
Maite Kramarz
University of Toronto
18:00
2h
Poster
Loop Invariants Using Neural Networks
Student Research Competition
Atticus Kuhn
University of Cambridge
Abhinandan Pal
University of Birmingham
Mirco Giacobbe
University of Birmingham
18:00
2h
Poster
Property Testing Trace Languages
Student Research Competition
Jed Koh Jin Keat
National University of Singapore
18:00
2h
Poster
Optimizing Asynchronous Rust with Hydroflow
Student Research Competition
Ryan Alameddine
University of California, Berkeley
18:00
2h
Poster
Relational Hoare Logic for Sequential Program Verification
Student Research Competition
Shushu Wu
Shanghai Jiao Tong University
18:00
2h
Poster
Expanding the Scope of Grammar-Based Enumerative Testing
Student Research Competition
Thea Kjeldsmark
University of California, Irvine
18:00
2h
Poster
System $F^\omega$ with Coherent Implicit Resolution
Student Research Competition
Eugene Flesselle
EPFL
Pre-print
18:00
2h
Poster
The Store-Order Consistency Testing Problem for C-like Memory Models
Student Research Competition
Grace Tan
National University of Singapore
18:00
2h
Poster
Formalizing Representation Transformations: A Case Study of Bit Vector Types
Student Research Competition
Katherine Philip
Portland State University
19:30 - 22:00
Women @ POPL Dinner
Catering
at
Panzano Restaurant
19:30
2h30m
Dinner
Women @ POPL Dinner
Catering
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
10:00 - 10:40
Break
Catering
at
Breakroom
10:00
40m
Coffee break
Break
Catering
10:40 - 12:00
Probabilistic Programming 2
POPL
at
Marco Polo
Chair(s):
Simon Oddershede Gregersen
New York University
10:40
20m
Talk
Inference Plans for Hybrid Particle Filtering
POPL
Ellie Y. Cheng
MIT
Eric Atkinson
Guillaume Baudart
Inria
Louis Mandel
IBM Research, USA
Michael Carbin
Massachusetts Institute of Technology
11:00
20m
Talk
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
Distinguished Paper
POPL
Fabian Zaiser
University of Oxford
Andrzej Murawski
University of Oxford
C.-H. Luke Ong
NTU
Pre-print
11:20
20m
Talk
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
POPL
Philipp Stassen
Aarhus University
Rasmus Ejlers Møgelberg
IT University of Copenhagen
Maaike Annebet Zwart
IT University of Copenhagen
Alejandro Aguirre
Aarhus University
Lars Birkedal
Aarhus University
11:40
20m
Talk
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
POPL
Jialu Bao
Cornell University
Emanuele D'Osualdo
University of Konstanz
Azadeh Farzan
University of Toronto
Pre-print
10:40 - 12:00
Syntax and Editing
POPL
at
Peek-A-Boo
Chair(s):
Guido Salvaneschi
University of St. Gallen
10:40
20m
Talk
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
POPL
Ian Erik Varatalu
Tallinn University of Technology, Estonia
Margus Veanes
Microsoft Research
Juhan Ernits
Tallinn University of Technology
DOI
Media Attached
11:00
20m
Talk
Pantograph: A Fluid and Typed Structure Editor
POPL
Jacob Prinz
University of Maryland, College Park
Henry Blanchette
Leonidas Lampropoulos
University of Maryland, College Park
Pre-print
Media Attached
11:20
20m
Talk
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL
Michael D. Adams
National University of Singapore
Eric Griffis
University of Michigan
Thomas J. Porter
University of Michigan
Sundara Vishnu Satish
University of Michigan - Ann Arbor
Eric Zhao
Brown University
Cyrus Omar
University of Michigan
11:40
20m
Talk
Biparsers: Exact Printing for Data Synchronisation
POPL
Ruifeng Xie
Peking University
Tom Schrijvers
KU Leuven
Zhenjiang Hu
Peking University
12:00 - 13:20
Lunch
Catering
at
Four Square Ballroom
12:00
80m
Lunch
Lunch
Catering
12:00 - 13:20
Lunch
Catering
at
Hopscotch
12:00
80m
Lunch
Lunch
Catering
12:00 - 13:20
SIGPLAN EC Meeting
Catering
at
Kick the Can
12:00
80m
Lunch
SIGPLAN EC meeting
Catering
12:00 - 13:20
LGBTQ+ Lunch
Catering
at
Patty Cake
12:00
80m
Lunch
LGBTQ+ Lunch
Catering
13:20 - 14:40
SRC Finalist Presentations
Student Research Competition
at
Keep Away
13:20
13m
Talk
System $F^\omega$ with Coherent Implicit Resolution
Student Research Competition
Eugene Flesselle
EPFL
Pre-print
13:33
13m
Talk
Efficient Strong Simulation of High-level Quantum Gates
Student Research Competition
Adam Husted Kjelstrøm
13:46
13m
Talk
The Store-Order Consistency Testing Problem for C-like Memory Models
Student Research Competition
Grace Tan
National University of Singapore
14:00
13m
Talk
Wanco: WebAssembly AOT Compiler that supports Live Migration
Student Research Competition
Raiki Tamura
Kyoto University
14:13
13m
Talk
Optimizing Asynchronous Rust with Hydroflow
Student Research Competition
Ryan Alameddine
University of California, Berkeley
14:26
13m
Talk
Property Testing Trace Languages
Student Research Competition
Jed Koh Jin Keat
National University of Singapore
13:20 - 14:20
Decision Procedures
POPL
at
Marco Polo
Chair(s):
Naoki Kobayashi
University of Tokyo
13:20
20m
Talk
The Decision Problem for Regular First Order Theories
POPL
Umang Mathur
National University of Singapore
David Mestel
Maastricht University
Mahesh Viswanathan
University of Illinois at Urbana-Champaign
Link to publication
DOI
Pre-print
13:40
20m
Talk
A Primal-Dual Perspective on Program Verification Algorithms
Distinguished Paper
POPL
Takeshi Tsukada
Chiba University
Hiroshi Unno
Tohoku University
Oded Padon
Weizmann Institute of Science
Sharon Shoham
Tel Aviv University
14:00
20m
Talk
Dis/Equality Graphs
POPL
George Zakhour
University of St. Gallen
Pascal Weisenburger
University of St. Gallen
Jahrim Gabriele Cesario
University of St. Gallen
Guido Salvaneschi
University of St. Gallen
Link to publication
DOI
Pre-print
13:20 - 14:20
Program Logics 1
POPL
at
Peek-A-Boo
Chair(s):
Derek Dreyer
MPI-SWS
13:20
20m
Talk
Program logics à la carte
POPL
Max Vistrup
ETH Zurich
Michael Sammler
Institute of Science and Technology Austria
Ralf Jung
ETH Zurich
13:40
20m
Talk
On Extending Incorrectness Logic with Backwards Reasoning
POPL
Freek Verbeek
Open Universiteit & Virginia Tech
Md Syadus Sefat
Virginia Tech
Zhoulai Fu
State University of New York, Korea
Binoy Ravindran
Virginia Tech
14:00
20m
Talk
A Demonic Outcome Logic for Randomized Nondeterminism
POPL
Noam Zilberstein
Cornell University
Dexter Kozen
Cornell University
Alexandra Silva
Cornell University
Joseph Tassarotti
New York University
14:20 - 15:00
Break
Catering
at
Breakroom
14:20
40m
Coffee break
Break
Catering
15:00 - 16:20
Types 1
POPL
at
Marco Polo
Chair(s):
Stephanie Weirich
University of Pennsylvania
15:00
20m
Talk
A Dependent Type Theory for Meta-programming with Intensional Analysis
POPL
Jason Z. S. Hu
Amazon Web Services, USA
Brigitte Pientka
McGill University
15:20
20m
Talk
Avoiding signature avoidance in ML modules with zippers
POPL
Clément Blaudeau
Inria
Didier Rémy
Inria
Gabriel Radanne
Inria
15:40
20m
Talk
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL
Shengyi Jiang
The University of Hong Kong
Chen Cui
University of Hong Kong
Bruno C. d. S. Oliveira
University of Hong Kong
16:00
20m
Talk
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
POPL
Taro Sekiyama
National Institute of Informatics; SOKENDAI
Hiroshi Unno
Tohoku University
15:00 - 16:20
Concurrency
POPL
at
Peek-A-Boo
Chair(s):
Andreas Pavlogiannis
Aarhus University
15:00
20m
Talk
Data Race Freedom à la Mode
Distinguished Paper
POPL
Aina Linn Georges
Max Planck Institute for Software Systems (MPI-SWS)
Benjamin Peters
MPI-SWS
Laila Elbeheiry
MPI-SWS
Leo White
Jane Street
Stephen Dolan
Jane Street
Richard A. Eisenberg
Jane Street
Chris Casinghino
Jane Street
François Pottier
Inria
Derek Dreyer
MPI-SWS
15:20
20m
Talk
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL
Pavel Golovin
MPI-SWS
Michalis Kokologiannakis
ETH Zurich
Viktor Vafeiadis
MPI-SWS
15:40
20m
Talk
Relaxed Memory Concurrency Re-executed
Distinguished Paper
Remote
POPL
Evgenii Moiseenko
JetBrains Research
Matteo Meluzzi
TU Delft, the Netherlands
Innokentii Meleshchenko
JetBrains Research, Neapolis University Pafos, Cyprus
Ivan Kabashnyi
JetBrains Research, Constructor University Bremen, Germany
Anton Podkopaev
JetBrains Research, Constructor University
Soham Chakraborty
TU Delft
16:00
20m
Talk
Model Checking C/C++ with Mixed-Size Accesses
POPL
Iason Marmanis
MPI-SWS
Michalis Kokologiannakis
ETH Zurich
Viktor Vafeiadis
MPI-SWS
16:20 - 17:00
Break
Catering
at
Breakroom
16:20
40m
Coffee break
Break
Catering
17:00 - 17:40
Quantum Computing 2
POPL
at
Marco Polo
Chair(s):
Jens Palsberg
University of California, Los Angeles (UCLA)
17:00
20m
Talk
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
POPL
Kengo Hirata
University of Edinburgh
Chris Heunen
University of Edinburgh
DOI
Pre-print
17:20
20m
Talk
Verifying Quantum Circuits with Level-Synchronized Tree Automata
POPL
Parosh Aziz Abdulla
Uppsala University, Sweden
Yo-Ga Chen
Academia Sinica
Yu-Fang Chen
Academia Sinica
Lukáš Holík
Brno University of Technology
Ondřej Lengál
Brno University of Technology
Jyun-Ao Lin
National Taipei University of Technology
Fang-Yi Lo
Academia Sinica
Wei-Lun Tsai
Academia Sinica
17:00 - 17:40
Kleene Algebra with Tests
POPL
at
Peek-A-Boo
Chair(s):
Chenyu Zhou
University of Southern California
17:00
20m
Talk
CF-GKAT: Efficient Validation of Control-Flow Transformations
POPL
Cheng Zhang
University College London (UCL)
Tobias Kappé
LIACS, Leiden University
David E. Narváez
Virginia Tech
Nico Naus
Open University of The Netherlands & Virginia Tech
17:20
20m
Talk
Algebras for Deterministic Computation are Inherently Incomplete
POPL
Balder ten Cate
ILLC, University of Amsterdam
Tobias Kappé
LIACS, Leiden University
17:50 - 19:00
SIGPLAN Awards, PC Chair's Report, and Business Meeting
POPL
at
Marco Polo
17:50
70m
Awards
SIGPLAN Awards, PC Chair's Report, and Business Meeting
POPL
Fri 24 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:00
Keynote
POPL
at
Marco Polo
09:00
60m
Talk
Welcome to Quantum 3.0!
POPL
Jens Palsberg
University of California, Los Angeles (UCLA)
10:00 - 10:40
Break
Catering
at
Breakroom
10:00
40m
Coffee break
Break
Catering
10:40 - 12:00
Synthesis and Compilation
POPL
at
Marco Polo
Chair(s):
Alexander K. Lew
Massachusetts Institute of Technology
10:40
20m
Talk
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
POPL
Roland Leißa
University of Mannheim, School of Business Informatics and Mathematics
Marcel Ullrich
Saarland University, Saarland Informatics Campus
Joachim Meyer
Saarland University, Saarland Informatics Campus
Sebastian Hack
Saarland University, Saarland Informatics Campus
Link to publication
Pre-print
11:00
20m
Talk
Simple Linear Loops: Algebraic Invariants and Applications
POPL
Rida Ait El Manssour
CNRS & IRIF, Paris
George Kenison
Liverpool John Moores University
Mahsa Shirmohammadi
CNRS & IRIF, Paris
Anton Varonka
TU Wien
11:20
20m
Talk
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
POPL
Yufan Cai
National University of Singapore
Zhe Hou
Griffith University
David Sanan
Singapore Institute of Technology
Xiaokun Luan
Peking University
Yun Lin
Shanghai Jiao Tong University
Jun Sun
Singapore Management University
Jin Song Dong
National University of Singapore
11:40
20m
Talk
Tail Modulo Cons, OCaml, and Relational Separation Logic
Remote
POPL
Clément Allain
INRIA
Frédéric Bour
Tarides
Basile Clément
OCamlPro
François Pottier
Inria
Gabriel Scherer
Université Paris Cité - Inria - CNRS
10:40 - 12:00
Types 2
POPL
at
Peek-A-Boo
Chair(s):
Mae Milano
Princeton University
10:40
20m
Talk
Affect: An Affine Type and Effect System
Distinguished Paper
POPL
Orpheas van Rooij
University of Edinburgh
Robbert Krebbers
Radboud University Nijmegen
Pre-print
11:00
20m
Talk
A modal deconstruction of Löb induction
POPL
Daniel Gratzer
Aarhus University
11:20
20m
Talk
QuickSub: Efficient Iso-Recursive Subtyping
POPL
Litao Zhou
University of Hong Kong
Bruno C. d. S. Oliveira
University of Hong Kong
11:40
20m
Talk
Generic Refinement Types
POPL
Nico Lehmann
UCSD
Cole Kurashige
UCSD
Nikhil Akiti
UCSD
Niroop Krishnakumar
UCSD
Ranjit Jhala
UCSD
12:00 - 13:20
Lunch
Catering
at
Four Square Ballroom
12:00
80m
Lunch
Lunch
Catering
12:00 - 13:20
Lunch
Catering
at
Hopscotch
12:00 - 13:20
URM Lunch
Catering
at
Patty Cake
12:00
80m
Lunch
URM Lunch
Catering
13:20 - 14:20
Verification 2
POPL
at
Marco Polo
Chair(s):
Zhong Shao
Yale University
13:20
20m
Talk
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
POPL
Yonghyun Kim
Seoul National University, South Korea
Minki Cho
Seoul National University
Jaehyung Lee
Seoul National University
Jinwoo Kim
Seoul National University
Taeyoung Yoon
Seoul National University
Youngju Song
MPI-SWS
Chung-Kil Hur
Seoul National University
13:40
20m
Research paper
Formalising Graph Algorithms with Coinduction
POPL
Donnacha Oisín Kidney
Imperial College London
Nicolas Wu
Imperial College London
Link to publication
DOI
Pre-print
14:00
20m
Talk
VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
POPL
Yoonseung Kim
Yale University
Sung-Hwan Lee
Seoul National University
Yonghyun Kim
Seoul National University, South Korea
Chung-Kil Hur
Seoul National University
13:20 - 14:20
Program Logics 2
POPL
at
Peek-A-Boo
Chair(s):
Thibault Dardinier
ETH Zurich
13:20
20m
Talk
BiSikkel: A Multimode Logical Framework in Agda
POPL
Joris Ceulemans
KU Leuven
Andreas Nuyts
KU Leuven, Belgium
Dominique Devriese
KU Leuven
DOI
13:40
20m
Talk
Calculational Design of Hyperlogics by Abstract Interpretation
POPL
Patrick Cousot
Jeffery Wang
CIMS, New York University
14:00
20m
Talk
A Taxonomy of Hoare-Like Logics
POPL
Lena Verscht
RWTH Aachen University; Saarland University
Benjamin Lucien Kaminski
Saarland University; University College London
Link to publication
Pre-print
14:20 - 15:00
Break
Catering
at
Breakroom
14:20
40m
Coffee break
Break
Catering
15:00 - 16:20
Concurrency 2
POPL
at
Marco Polo
Chair(s):
Umang Mathur
National University of Singapore
15:00
20m
Talk
Flo: a Semantic Foundation for Progressive Stream Processing
POPL
Shadaj Laddad
University of California at Berkeley
Alvin Cheung
University of California at Berkeley
Joseph M. Hellerstein
UC Berkeley
Mae Milano
Princeton University
Pre-print
15:20
20m
Talk
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
POPL
Thien Udomsrirungruang
University of Oxford
Nobuko Yoshida
University of Oxford
Pre-print
15:40
20m
Talk
Semantic Logical Relations for Timed Message-Passing Protocols
POPL
Yue Yao
Carnegie Mellon University
Grant Iraci
University at Buffalo
Cheng-En Chuang
University at Buffalo
Stephanie Balzer
Carnegie Mellon University
Lukasz Ziarek
University at Buffalo
16:00
20m
Talk
Reachability Analysis of the Domain Name System
POPL
Dhruv Nevatia
ETH Zurich
Si Liu
ETH Zurich
David Basin
ETH Zurich
15:00 - 16:20
Theory
POPL
at
Peek-A-Boo
Chair(s):
Neel Krishnaswami
University of Cambridge
15:00
20m
Talk
The Duality of λ-Abstraction
POPL
Vikraman Choudhury
Università di Bologna & Inria OLAS
Simon J. Gay
University of Glasgow, UK
Link to publication
DOI
Media Attached
15:20
20m
Talk
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
POPL
Naoki Kobayashi
University of Tokyo
15:40
20m
Talk
Interaction Equivalence
POPL
Beniamino Accattoli
Inria & Ecole Polytechnique
Adrienne Lancelot
Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité
Giulio Manzonetto
Université Paris Cité
Gabriele Vanoni
IRIF, Université Paris Cité
16:00
20m
Talk
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Distinguished Paper
POPL
Jan van Brügge
Heriot-Watt University
James McKinna
Heriot-Watt University
Andrei Popescu
University of Sheffield
Dmitriy Traytel
University of Copenhagen
Link to publication
DOI
Pre-print
16:20 - 17:00
Break
Catering
at
Breakroom
16:20
40m
Coffee break
Break
Catering
17:00 - 18:00
Speculative Execution
POPL
at
Marco Polo
Chair(s):
Viktor Vafeiadis
MPI-SWS
17:00
20m
Talk
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
POPL
Xaver Fabian
CISPA
Marco Patrignani
University of Trento
Marco Guarnieri
IMDEA Software Institute
Michael Backes
Cispa Helmholtz Center for Information Security
Link to publication
17:20
20m
Talk
Preservation of speculative constant-time by compilation
POPL
Santiago Arranz Olmos
Max Planck Institute for Security and Privacy
Gilles Barthe
MPI-SP; IMDEA Software Institute
Lionel Blatter
Max Planck Institute for Security and Privacy
Benjamin Gregoire
INRIA
Vincent Laporte
Inria
17:40
20m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL
Sören van der Wall
TU Braunschweig
Roland Meyer
TU Braunschweig
Link to publication
DOI
17:00 - 18:00
Proof Assistants
POPL
at
Peek-A-Boo
Chair(s):
Joomy Korkut
Bloomberg LP
17:00
20m
Talk
Progressful Interpreters for Efficient WebAssembly Mechanisation
POPL
Xiaojia Rao
Imperial College London
Stefan Radziuk
Imperial College London
Conrad Watt
Nanyang Technological University
Philippa Gardner
Imperial College London
Link to publication
DOI
17:20
20m
Talk
Unifying compositional verification and certified compilation with a three-dimensional refinement algebra
POPL
Yu Zhang
Jérémie Koenig
Yale University
Zhong Shao
Yale University
Yuting Wang
Shanghai Jiao Tong University
17:40
20m
Talk
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Remote
POPL
Josselin Poiret
Nantes Université, Inria
Gaetan Gilbert
Kenji Maillard
Inria
Pierre-Marie Pédrot
INRIA
Matthieu Sozeau
Inria
Nicolas Tabareau
Inria
Éric Tanter
University of Chile
Sat 25 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Session 1
PLanQC
at
Keep Away
Chair(s):
Jennifer Paykin
Intel
09:00
45m
Keynote
Unlocking quantum potential with software and compilers
Keynote
PLanQC
Kaitlin Smith
Northwestern University
09:46
22m
Talk
HUGR: A Quantum-Classical Intermediate Representation
Talk
PLanQC
Seyon Sivarajah
Quantinuum
Mark Koch
Quantinuum
Agustin Borgna
Quantinuum
Alan Lawrence
Quantinuum
Alec Edgington
Quantinuum
Douglas Wilson
Quantinuum
Craig Roy
Quantinuum
Luca Mondada
University of Oxford
Lukas Heidemann
Quantinuum
Ross Duncan
Quantinuum
File Attached
10:08
22m
Talk
QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuits
Talk
PLanQC
Ilan Iwumbwe
Imperial College London
Benny Zong Liu
Imperial College London
John Wickerson
Imperial College London
Media Attached
File Attached
09:00 - 10:30
Session 1
WITS
at
Kick the Can
09:00
60m
Keynote
Invited Talk: Type inference in OCaml and GHC using Levels
WITS
Richard A. Eisenberg
Jane Street
10:00
30m
Talk
Towards Generic Higher-Order Unification Implementations in Haskell
Remote
WITS
Nikolai Kudasov
Innopolis University
Artem Starikov
Innopolis University
Fedor Ivanov
Innopolis University
Damir Alfiatonov
Innopolis University
File Attached
09:00 - 10:30
Session 1
CoqPL
at
Peek-A-Boo
Chair(s):
Kathrin Stark
Heriot-Watt University
09:00
50m
Keynote
Elpi: rule-based meta-languge for Rocq
CoqPL
Enrico Tassi
INRIA
Media Attached
File Attached
09:50
20m
Talk
Implementing OCaml APIs in Coq
CoqPL
Joshua M. Cohen
Princeton University
File Attached
10:10
20m
Talk
Towards general white-box automation: a typeclass-guided context cleaner
CoqPL
Thibaut Pérami
University of Cambridge
File Attached
10:30 - 11:00
Break
Catering
at
Breakroom
10:30
30m
Coffee break
Break
Catering
11:00 - 12:30
Session 2
PLanQC
at
Keep Away
Chair(s):
Peng Fu
University of South Carolina
11:00
22m
Talk
The Quantum Abstract Machine
Talk
PLanQC
Le Chang
University of Maryland, College Park
Liyi Li
Iowa State University
Rance Cleaveland
University of Maryland
Mingwei Zhu
University of Maryland, College Park
Xiaodi Wu
University of Maryland
File Attached
11:22
22m
Talk
Algebraic and denotational semantics for Classically Controlled Quantum Communication
Talk
PLanQC
Theo Wang
University of Cambridge, University of Oxford
Sam Staton
University of Oxford
File Attached
11:45
22m
Talk
Towards Quantum Multiparty Session Types
Talk
PLanQC
Ivan Lanese
University of Bologna/INRIA
Ugo Dal Lago
University of Bologna & INRIA Sophia Antipolis
Vikraman Choudhury
Università di Bologna & Inria OLAS
File Attached
12:07
22m
Talk
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
Talk
PLanQC
Yusuke Matsushita
Kyoto University
Kengo Hirata
University of Edinburgh
Ryo Wakizaka
Kyoto University
File Attached
11:00 - 12:30
Session 2
WITS
at
Kick the Can
11:00
30m
Talk
Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Remote
WITS
Nikolai Kudasov
Innopolis University
Anastasia Smirnova
Innopolis University
Vladislav Deryabkin
Innopolis University
Diana Tomilovskaia
Innopolis University
Ekaterina Maksimova
Innopolis University
File Attached
11:30
30m
Talk
McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
WITS
Junyoung Jang
McGill University
Jason Z. S. Hu
Amazon Web Services, USA
Antoine Gaulin
McGill University
Brigitte Pientka
McGill University
Pre-print
File Attached
12:00
30m
Talk
Eta conversion for the unit type (is still not that simple)
Remote
WITS
András Kovács
University of Gothenburg and Chalmers University of Technology
File Attached
11:00 - 12:30
Session 2
CoqPL
at
Peek-A-Boo
Chair(s):
Benjamin Delaware
Purdue University
11:00
70m
Panel
Session with the Coq Development Team
CoqPL
Matthieu Sozeau
Inria
Nicolas Tabareau
Inria
Enrico Tassi
INRIA
Yves Bertot
INRIA
12:10
20m
Talk
Vellvm: Formalizing the Informal
CoqPL
Calvin Beck
University of Pennsylvania, USA
Hanxi Chen
University of Pennsylvania
Steve Zdancewic
University of Pennsylvania
File Attached
12:30 - 14:00
Lunch
Catering
at
Four Square Ballroom
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:30
Session 3
PLanQC
at
Keep Away
Chair(s):
Ross Duncan
Quantinuum
14:00
22m
Talk
Verifying the Equivalence of Parameterized Quantum Circuits
Talk
PLanQC
Scott Wesley
Dalhousie University
Neil Julien Ross
Dalhousie University
File Attached
14:22
22m
Talk
An Automata-based Framework for Quantum Circuit Verification
Talk
PLanQC
Parosh Aziz Abdulla
Uppsala University, Sweden
Yo-Ga Chen
Academia Sinica
Yu-Fang Chen
Academia Sinica
Kai-Min Chung
Academia Sinica
Lukáš Holík
Brno University of Technology
Ondřej Lengál
Brno University of Technology
Jyun-Ao Lin
National Taipei University of Technology
Fang-Yi Lo
Academia Sinica
Wei-Lun Tsai
Academia Sinica
Di-De Yen
Academia Sinica
File Attached
14:45
45m
Poster
Poster Session
PLanQC
14:00 - 15:30
Session 3
WITS
at
Kick the Can
14:00
30m
Other
Collaboration Time 1
WITS
14:30
30m
Talk
Semantic Analysis of Normalisation for Directional Logic Programming
Remote
WITS
Vikraman Choudhury
Università di Bologna & Inria OLAS
Neel Krishnaswami
University of Cambridge
Ariadne Si Suo
University of Cambridge
File Attached
15:00
30m
Talk
Incremental Bidirectional Typing via Order Maintenance
WITS
Thomas J. Porter
University of Michigan
Marisa Kirisame
University of Utah
Liam Mulcahy
University of Michigan
Pavel Panchekha
University of Utah
Cyrus Omar
University of Michigan
File Attached
14:00 - 15:30
Session 3
CoqPL
at
Peek-A-Boo
Chair(s):
Benjamin Delaware
Purdue University
14:00
22m
Talk
Towards Verified Linear Algebra Programs Through Equivalence
CoqPL
Yihan Yang
Harvey Mudd College
Mohit Tekriwal
Lawrence Livermore National Laboratory
John Sarracino
Lawrence Livermore National Laboratory
Matthew Sottile
Lawrence Livermore National Laboratory
Ignacio Laguna
Lawrence Livermore National Laboratory
File Attached
14:22
22m
Talk
A Framework of Differential Operators
CoqPL
Runqing Xu
Sebastian Erdweg
JGU Mainz
File Attached
14:45
22m
Talk
A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
CoqPL
Tarakaram Gollamudi
None
Jules Jacobs
Cornell University
Yue Yao
Carnegie Mellon University
Stephanie Balzer
Carnegie Mellon University
File Attached
15:07
22m
Talk
Formal Verification of a Software Defined Delay-Tolerant Network
CoqPL
Jan-Paul Ramos-Davila
Cornell University
File Attached
15:30 - 16:00
Break
Catering
at
Breakroom
15:30
30m
Coffee break
Break
Catering
16:00 - 17:30
Session 4
PLanQC
at
Keep Away
Chair(s):
Robert Rand
University of Chicago
16:00
22m
Talk
Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs (Extended Abstract)
Talk
Remote
PLanQC
Zhicheng Zhang
University of Technology Sydney
Mingsheng Ying
Institute of Software at Chinese Academy of Sciences; Tsinghua University
File Attached
16:22
22m
Talk
Programming with Projective Cliffords
Talk
PLanQC
Jennifer Paykin
Intel
Sam Winnick
University of Waterloo
File Attached
16:45
22m
Talk
Proto-Quipper with Reversing and Control
Talk
PLanQC
Peng Fu
University of South Carolina
Kohei Kishida
University of Illinois at Urbana-Champaign
Neil Julien Ross
Dalhousie University
Peter Selinger
Dalhousie University
File Attached
17:07
22m
Talk
Imperative Quantum Programming with Ownership and Borrowing in Guppy
Talk
PLanQC
Mark Koch
Quantinuum
Agustin Borgna
Quantinuum
Craig Roy
Quantinuum
Alan Lawrence
Quantinuum
Kartik Singhal
Quantinuum
Seyon Sivarajah
Quantinuum
Ross Duncan
Quantinuum
Media Attached
File Attached
16:00 - 17:30
Session 4
WITS
at
Kick the Can
16:00
30m
Other
Collaboration Time 2
WITS
16:30
30m
Talk
Formalizing locally nameless syntax with cofinite quantification
WITS
Elif Uskuplu
Indiana University, Bloomington
File Attached
17:00
30m
Other
Closing
WITS
16:00 - 17:30
Session 4 (16:00 - 17:30)
CoqPL
at
Peek-A-Boo
Chair(s):
Qianchuan Ye
University at Buffalo, SUNY
16:00
22m
Talk
Towards Automated Verification of LLM-Synthesized C Programs
CoqPL
Prasita Mukherjee
Benjamin Delaware
Purdue University
File Attached
16:22
23m
Talk
CoqNFU: Towards Formalizing NFU in Coq
CoqPL
Marko Doko
Heriot-Watt University, UK
Vedran Čačić
File Attached
16:45
22m
Talk
Towards Mining Robust Coq Proof Patterns
Remote Participation
CoqPL
Cezary Kaliszyk
University of Melbourne
Xuan-Bach D. Le
University of Melbourne
Christine Rizkallah
University of Melbourne
File Attached
17:07
22m
Talk
Formal Verification of Quantum Stabilizer Code
Remote Participation
CoqPL
Qiuyi Feng
Udaya Parampalli
Christine Rizkallah
University of Melbourne
File Attached
Get Calendar (iCal)
iCalendar subscription service for your personal schedule
You first need to have starred events (
) in order to use the iCalendar subscription service.
Currently Viewed Program
Downloads the currently viewed program (with filters applied) in iCal format
Close
Fri 24 Apr 16:35