POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Thu 23 Jan 2025 17:00 - 17:20 at Marco Polo - Quantum Computing 2

Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated as a linear type, automatic uncomputation enables the programmer to treat it as an affine type to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts. Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.

This program is tentative and subject to change.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

17:00 - 17:40
Quantum Computing 2POPL at Marco Polo
17:00
20m
Talk
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
POPL
Kengo Hirata University of Edinburgh, Chris Heunen University of Edinburgh
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