proto-quipper-d

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 …

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper

We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the …

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 …