proto-quipper-m

Linear Dependent Type Theory for Quantum Programming Languages

Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages …

Proto-Quipper with dynamic lifting

Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting, which is …

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

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 …

Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data -- qubits -- into classical data -- …

Quantum CPOs

We introduce the monoidal closed category qCPO of quantum cpos, whose objects are "quantized" analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the …

On a Categorically Sound Quantum Programming Language for Circuit Description

This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not so distant future has resulted in a flurry of activity in the development of quantum …

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract

Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages …

Enriching a Linear/Non-Linear Lambda Calculus: A Programming Language for String Diagrams

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus …

A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)

Quipper is a practical programming language for describing families of quantum circuits. In this paper, we formalize a small, but useful fragment of Quipper called Proto-Quipper-M. Unlike its parent Quipper, this language is type-safe and has a …