Fri 17 Jun 2022 13:30 - 13:50 at Cockatoo - Special Effects Chair(s): Steven Holtzen

Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns.

In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation.

We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification.

We evaluate Twist’s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%. DOI

Fri 17 Jun

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

13:30 - 14:50
Special EffectsSIGPLAN Track at Cockatoo
Chair(s): Steven Holtzen Northeastern University
13:30
20m
Talk
(POPL 2022) Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
SIGPLAN Track
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Authorizer link Pre-print
13:50
20m
Talk
(ICFP 2020) Compiling effect handlers in capability-passing style
SIGPLAN Track
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tuebingen
Link to publication DOI Authorizer link Pre-print
14:10
20m
Talk
(POPL 2021) Intensional Datatype Refinement
SIGPLAN Track
Eddie Jones University of Bristol, Steven Ramsay University of Bristol
14:30
20m
Talk
(POPL 2021) A Verified Optimizer for Quantum Circuits
SIGPLAN Track
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD, Michael Hicks University of Maryland at College Park