Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

A functional quantum programming language

Thorsten Altenkirch, Jonathan Grattage

Published Sep 11, 2004• 192 citations
OpenAlex

Abstract

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 realizable 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. 1

Related papers

A Functional Quantum Programming Language

T. Altenkirch, Jonathan Grattage

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.

arXiv:quant-ph/0409065•ACM/IEEE Symposium on Logic in Computer Science (LICS)•Oct 11, 2006•117 citations

Compilation to Quantum Circuits for a Language with Quantum Data and Control

Yannis Rouselakis, Nikolaos Papaspyrou, Yiannis Tsiouris +1 more

Abstract—In this paper we further investigate nQML, a functional quantum programming language that follows the “quantum data and control ” paradigm. We define a semantics for nQML, which translates programs to quantum circuits in the category FQC of finite quantum computations, following the approach of Altenkirch and Grattage’s QML. This semantics, which coincides with the denotational semantics for nQML over density matrices and unitary transformations, serves as a compiler from nQML programs to quantum circuits. We also provide an implementation of this compiler, written in Haskell, as well as an interpreter for quantum circuits. I.

•Nov 3, 2015•3 citations

Reversibility for Quantum Programming Language QML

Nely Plata César, J. Raymundo Marcial‐Romero, José Antonio Hernández Servín

We present an extension of the denotational semantic model of the quantum programming language QML, to which computational reversibility is incorporated. The semantics of QML is defined in a functional setting which consider classical and quantum data, to which we add inverse functions. Additionally we incorporate into the semantics a history track which allows reversibility in QML. From the generation and processing of the history track and the final result of a program, the rules for executing reversibility allow to compute the original input data. This work contributes to the study of reversibility in quantum programming languages and considering that there is not yet a quantum computer in which the language can be implemented, this history and the proposed inverse functions are not trivial and allow us to determine that this language is reversible.

IEEE Latin America Transactions•Oct 1, 2020•1 citation

Lenguaje de programación cuántico QML con historial, reversibilidad y cálculo lambda con mediciones

Nely Plata César

Research in quantum computing allows us to think about computing in a new and different way, having the ambition to solve problems more efficiently than with classical computing. Now a days, conventional tasks cannot be practically developed in a quantum computer, however, it is possible to think and develop abstractions of them, for example through quantum programming languages, being the core of this research, in particular the Quantum Meta Language (QML). We present a semantic model that incorporates reversibility via a history track for the quantum programming language QML, considering classical and quantum data, omitting measurements. With the history, the reversibility can be explicitly and naturally applied from the proposed rules. The language is worked first with classical data and extrapolated to quantum data. Also, the QML language and quantum lambda calculus were linked, giving as product a syntax with quantum measurements, operational semantics, typing rules and some formal proofs.

•Jun 1, 2020•0 citations

A functional programming language for quantum computation with classical control

Benoît Valiron

The objective of this thesis is to develop a functional programming language for quantum computers based on the QRAM model, following the work of P. Selinger (2004) on quantum flow-charts. We construct a lambda-calculus without side-effects to deal with quantum bits. We equip this calculus with a probabilistic call-by-value operational semantics. Since quantum information cannot be duplicated due to the no-cloning property, we need a resource-sensitive type system. We develop it based on affine intuitionistic linear logic. Unlike the quantum lambda-calculus proposed by Van Tonder (2003, 2004), the resulting lambda-calculus has only one lambda-abstraction, linear and non-linear abstractions being encoded in the type system. We also integrate classical and quantum data types within our language. The main results of this work are the subject-reduction of the language and the construction of a type inference algorithm.

•Jan 1, 2004•17 citations

Towards a quantum programming language

Peter Selinger

We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.

Mathematical Structures in Computer Science•Aug 1, 2004•478 citations
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 realizable 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. 1
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.
Abstract—In this paper we further investigate nQML, a functional quantum programming language that follows the “quantum data and control ” paradigm. We define a semantics for nQML, which translates programs to quantum circuits in the category FQC of finite quantum computations, following the approach of Altenkirch and Grattage’s QML. This semantics, which coincides with the denotational semantics for nQML over density matrices and unitary transformations, serves as a compiler from nQML programs to quantum circuits. We also provide an implementation of this compiler, written in Haskell, as well as an interpreter for quantum circuits. I.
We present an extension of the denotational semantic model of the quantum programming language QML, to which computational reversibility is incorporated. The semantics of QML is defined in a functional setting which consider classical and quantum data, to which we add inverse functions. Additionally we incorporate into the semantics a history track which allows reversibility in QML. From the generation and processing of the history track and the final result of a program, the rules for executing reversibility allow to compute the original input data. This work contributes to the study of reversibility in quantum programming languages and considering that there is not yet a quantum computer in which the language can be implemented, this history and the proposed inverse functions are not trivial and allow us to determine that this language is reversible.
Research in quantum computing allows us to think about computing in a new and different way, having the ambition to solve problems more efficiently than with classical computing. Now a days, conventional tasks cannot be practically developed in a quantum computer, however, it is possible to think and develop abstractions of them, for example through quantum programming languages, being the core of this research, in particular the Quantum Meta Language (QML). We present a semantic model that incorporates reversibility via a history track for the quantum programming language QML, considering classical and quantum data, omitting measurements. With the history, the reversibility can be explicitly and naturally applied from the proposed rules. The language is worked first with classical data and extrapolated to quantum data. Also, the QML language and quantum lambda calculus were linked, giving as product a syntax with quantum measurements, operational semantics, typing rules and some formal proofs.
The objective of this thesis is to develop a functional programming language for quantum computers based on the QRAM model, following the work of P. Selinger (2004) on quantum flow-charts. We construct a lambda-calculus without side-effects to deal with quantum bits. We equip this calculus with a probabilistic call-by-value operational semantics. Since quantum information cannot be duplicated due to the no-cloning property, we need a resource-sensitive type system. We develop it based on affine intuitionistic linear logic. Unlike the quantum lambda-calculus proposed by Van Tonder (2003, 2004), the resulting lambda-calculus has only one lambda-abstraction, linear and non-linear abstractions being encoded in the type system. We also integrate classical and quantum data types within our language. The main results of this work are the subject-reduction of the language and the construction of a type inference algorithm.
We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.