QML is a functional language for quantum computations on finite types. The language introduces quantum data and quantum control structures, and integrates reversible and irreversible quantum computation. QML is based on strict linear logic, hence weakenings, which may lead to decoherence, have to be explicit.
The design of QML is guided by its categorical semantics: QML programs are interpreted as morphisms in the category FQC of Finite Quantum Computations. This provides a constructive semantics of irreversible quantum computations realisable as quantum gates. The relationships between the category FQC and its classical reversible counterpart, FCC (Finite Classical Computations), are also explored.
The operational semantics of QML programs is presented using standard quantum circuits, while a denotational semantics is given using superoperators.
This research has been supported by the EPSRC, via the MathFIT initiative, grant numberGR/S30818/01. We are also involved in the EPSRC research network on the Semantics of Quantum Computation ( QNET ).