Fri 20 Jan 2023 10:45 - 11:10 at Square - Quantum Computing Chair(s): Ugo Dal Lago

We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum and classical effects. For example, one can use sum types to implement the direct sum of linear operators, exception-handling syntax to implement projective measurements, and aliasing to induce entanglement. Further, Qunity takes advantage of the overlooked BQP subroutine theorem, allowing one to construct reversible subroutines from irreversible quantum algorithms through the uncomputation of "garbage" outputs. Unlike existing languages that enable quantum aspects with separate add-ons (like a classical language with quantum gates bolted on), Qunity provides a unified syntax and a novel denotational semantics that guarantees that programs are quantum mechanically valid. We present Qunity's syntax, type system, and denotational semantics, showing how it can cleanly express several quantum algorithms. We also detail how Qunity can be compiled into a low-level qubit circuit language like OpenQASM, proving the realizability of our design.

Fri 20 Jan

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

10:45 - 12:00
Quantum ComputingPOPL at Square
Chair(s): Ugo Dal Lago University of Bologna; Inria
10:45
25m
Talk
Qunity: A Unified Language for Quantum and Classical Computing
POPL
Finn Voichick University of Maryland, Liyi Li University of Maryland, Robert Rand University of Chicago, Michael Hicks University of Maryland; Amazon
DOI Pre-print
11:10
25m
Talk
Proto-Quipper with Dynamic LiftingVirtual
POPL
Peng Fu Dalhousie University, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University
DOI
11:35
25m
Talk
CoqQ: Foundational Verification of Quantum ProgramsVirtual
POPL
Li Zhou MPI-SP; Institute of Software at Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Pierre-Yves Strub Meta, Junyi Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University
DOI