On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version)

TL;DR

This paper introduces Proto-Quipper-K, an extension of lambda-calculus for quantum circuit languages, featuring dynamic lifting and effectful types, with proven type soundness.

Contribution

It generalizes Proto-Quipper-M to include dynamic lifting through a rich effect and type system, enabling finer control in quantum circuit description languages.

Findings

Proves subject reduction for Proto-Quipper-K

Establishes progress and type soundness

Models dynamic lifting in quantum languages

Abstract

In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.