categorical model

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 …

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 …

Applying Quantitative Semantics to Higher-Order Quantum Computing

Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the language to …

Dagger Compact Closed Categories and Completely Positive Maps (Extended Abstract)

Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name "strongly compact closed categories", as an axiomatic framework for quantum mechanics. We present a graphical language for dagger compact closed …