A functional quantum programming language

Abstract

We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive semantics of irreversible quantum computations realisable as quantum gates. QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings explicit. Strict programs are free from decoherence and hence preserve superpositions and entanglement - which is essential for quantum parallelism.

15 pages. Final version, to appear in Logic in Computer Science 2005

References in corpus (2)

• A Lambda Calculus for Quantum Computation
• A lambda calculus for quantum computation with classical control

Cited by in corpus (36)

• Quantum walks: a comprehensive review
• Requirements for fault-tolerant factoring on an atom-optics quantum computer
• Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• Quantitative Robustness Analysis of Quantum Programs (Extended Version)
• Quantum Alternation: Prospects and Problems
• Tower: Data Structures in Quantum Superposition
• Toward Automatic Verification of Quantum Programs
• A logical analysis of entanglement and separability in quantum higher-order functions
• Integration of Quantum Accelerators with High Performance Computing -- A Review of Quantum Programming Tools
• Realizability in the Unitary Sphere
• On the Principles of Differentiable Quantum Programming Languages
• Weakly measured while loops: peeking at quantum states
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
• Universal construction of decoders from encoding black boxes
• A Modular Formalization of Reversibility for Concurrent Models and Languages
• A linear linear lambda-calculus
• A Parametric Framework for Reversible Pi-Calculi
• A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
• Modular quantum signal processing in many variables
• Completeness of algebraic CPS simulations
• Join Inverse Rig Categories for Reversible Functional Programming, and Beyond
• Sized Types for low-level Quantum Metaprogramming
• A concrete model for a typed linear algebraic lambda calculus
• A lambda calculus for density matrices with classical and probabilistic controls
• Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
• The Quantum Monadology
• A linear proof language for second-order intuitionistic linear logic
• Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
• Compositional Quantum Control Flow with Efficient Compilation in Qunity
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus
• Quantum Programming Without the Quantum Physics
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• QSSA: An SSA-based IR for Quantum Computing
• Quantum Circuits Are Just a Phase