An Algebra of Pure Quantum Programming

Abstract

We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation by evaluation approach. The current work focuses on the pure fragment of QML omitting measurements.

To appear in ENTCS, 3rd International Workshop on Quantum Programming Languages, 2005. 21 Pages

References in corpus (2)

• A Lambda Calculus for Quantum Computation
• Quantum Computation, Categorical Semantics and Linear Logic

Cited by in corpus (9)

• Lineal: A linear-algebraic Lambda-calculus
• Measurements and confluence in quantum lambda calculi with explicit qubits
• Defining Quantum Control Flow
• On the completeness of quantum computation models
• A HoTT Quantum Equational Theory (Extended Version)
• The Arrow Calculus as a Quantum Programming Language
• An overview of QML with a concrete implementation in Haskell
• Towards A Theory Of Quantum Computability
• QPCF: higher order languages and quantum circuits