POPL 2025
Sun 19 - Sat 25 January 2025
Denver, Colorado, United States
Toggle navigation
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
PLMW @ POPL
PLanQC
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
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PLanQC
Organizing Committee
Program Committee
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
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2025
(
series
) /
Curtis Hotel Denver
/
Room information: Red Rover
Venue
Curtis Hotel Denver
Room name
Red Rover
Floor
3
Capacity
110
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
This program is tentative and subject to change.
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-07:00) Mountain Time (US & Canada)
.
Use conference time zone: (GMT-07:00) Mountain Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Mon 20 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
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
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
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
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
Stateless model checking concurrent and distributed programs
Tutorials
at
Red Rover
09: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
Stateless model checking concurrent and distributed programs
Tutorials
at
Red Rover
11:00
90m
Tutorial
Stateless Model Checking Concurrent and Distributed Programs
Tutorials
P:
Michalis Kokologiannakis
ETH Zurich
,
P:
Viktor Vafeiadis
MPI-SWS
Wed 22 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
12:00 - 13:20
Mentoring Lunch
Catering
at
Red Rover
12:00
80m
Lunch
Mentoring Lunch
Catering
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
12:00 - 13:20
Lunch
Catering
at
Red Rover
12:00
80m
Lunch
Lunch
Catering
Fri 24 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
12:00 - 13:20
Lunch
Catering
at
Red Rover
Sat 25 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:30
Session 1
PLanQC
at
Red Rover
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
11:00 - 12:30
Session 2
PLanQC
at
Red Rover
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
14:00 - 15:30
Session 3
PLanQC
at
Red Rover
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
16:00 - 17:30
Session 4
PLanQC
at
Red Rover
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
Hide past events
Mon 20 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Red Rover
Tutorials
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
Viper: An Infrastructure for Automated Verification in Separation Logic
Tutorials
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tutorials
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Tue 21 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
Red Rover
Tutorials
Stateless model checking concurrent and distributed programs
Tutorials
Stateless model checking concurrent and distributed programs
Wed 22 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
30
13:00
30
Red Rover
Catering
Mentoring Lunch
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
30
13:00
30
Red Rover
Catering
Lunch
Fri 24 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
30
13:00
30
Red Rover
Catering
Lunch
Sat 25 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Red Rover
PLanQC
Session 1
PLanQC
Session 2
PLanQC
Session 3
PLanQC
Session 4
Hide past events
Mon 20 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Red Rover
POPL Tutorials
Viper: An Infrastructure for Automated Verification in Separation Logic
09:00 - 10:30
POPL Tutorials
Viper: An Infrastructure for Automated Verification in Separation Logic
11:00 - 12:30
POPL Tutorials
Verification of Distributed Protocols: Decidable Modeling and Invariant ...
14:00 - 15:30
POPL Tutorials
Verification of Distributed Protocols: Decidable Modeling and Invariant ...
16:00 - 17:30
Tue 21 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
Red Rover
POPL Tutorials
Stateless Model Checking Concurrent and Distributed Programs
09:00 - 10:30
POPL Tutorials
Stateless Model Checking Concurrent and Distributed Programs
11:00 - 12:30
Wed 22 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
15
30
45
13:00
15
30
45
Red Rover
POPL Catering
Mentoring Lunch
12:00 - 13:20
Thu 23 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
12:00
15
30
45
13:00
15
30
45
Red Rover
POPL Catering
Lunch
12:00 - 13:20
Sat 25 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Red Rover
PLanQC
Keynote
Unlocking quantum potential with software and compilers
09:00 - 09:45
PLanQC
Talk
HUGR: A Quantum-Classical Intermediate Representation
09:46 - 10:08
PLanQC
Talk
QuteFuzz: Fuzzing quantum compilers using randomly generated circuits w ...
10:08 - 10:30
PLanQC
Talk
The Quantum Abstract Machine
11:00 - 11:22
PLanQC
Talk
Algebraic and denotational semantics for Classically Controlled Quantum ...
11:22 - 11:45
PLanQC
Talk
Towards Quantum Multiparty Session Types
11:45 - 12:07
PLanQC
Talk
Concurrent Quantum Separation Logic for Fine-Grained Parallelism
12:07 - 12:30
PLanQC
Talk
Verifying the Equivalence of Parameterized Quantum Circuits
14:00 - 14:22
PLanQC
Talk
An Automata-based Framework for Quantum Circuit Verification
14:22 - 14:45
PLanQC
Poster Session
14:45 - 15:30
PLanQC
Talk
Remote
Quantum Register Machine: Efficient Implementation of Quantum Recursive ...
16:00 - 16:22
PLanQC
Talk
Programming with Projective Cliffords
16:22 - 16:45
PLanQC
Talk
Proto-Quipper with Reversing and Control
16:45 - 17:07
PLanQC
Talk
Imperative Quantum Programming with Ownership and Borrowing in Guppy
17:07 - 17:30
Hide past events
x
Mon 20 Jan 23:32