# Quantum Calculi--From Theory to Language Design
## 4 Foundational Quantum Programming Languages
### Quantum Lambda Calculi  
In Reference [16], [PERSON] rigorously defined a first-order quantum functional language. This paper represents a milestone for a part of the calculi developed in the following years and definitively founds the QRAM-based programming model, where only data (qubits) are superposed and where programs live in a standard classical world. Subsequently the author, in joint work with [PERSON] [3], defined a quantum \(\lambda\)-calculus with classical control, here dubbed \(\lambda_{sv}\), that we have briefly discussed in Section 2.3. The main goal of [PERSON] and [PERSON]'s work is to give the basis of a _typed_ quantum functional language, based on a call-by-value \(\lambda\)-calculus enriched with constants for unitary transformations and an explicit measurement operator which allows the program to observe the value of one qubit. Reductions are defined between _program states_, whose definition is similar to the one of configuration (Section 2.3). Because of the presence of measurement, the authors provide an operational semantics based on a probabilistic call-by-value evaluation. The type system of \(\lambda_{sv}\) is based on linear logic (linearity is extended to higher types), by distinguishing between duplicable and non-duplicable resources. The type system of \(\lambda_{sv}\) is based on linear logic (linearity is extended to higher types), by distinguishing between duplicable and non-duplicable resources. [PERSON] and [PERSON]'s type syntax is the following: \(A,B::=\alpha|X|!A|A\to B|\top|A\otimes B\) where \(\alpha\) ranges over a set of type constants, \(X\) ranges over a countable set of type variables, \(\rightarrow\) represents the linear implication and \(\top\) is the linear unit type. As previously said the authors restrict the system to be _affine_, that is, _contraction structural rule is not allowed_. The type system avoids run-time errors and is also equipped with subtyping rules, which provide a more refined control of the resources. \(\lambda_{sv}\) enjoys some good properties such as subject reduction and progress and a strong notion of _safety_. The authors also define a new interesting quantum type inference algorithm, based on the idea that a linear (quantum) type can be viewed as a decoration of an intuitionistic one. An example of \(\lambda_{sv}\) well-typed term, encoding the EPR circuit is \(\lambda_{sv}\) as \(EPR=\lambda x.CNOT\langle H(\mathsf{nw}(0)),\mathsf{nw}(0)\rangle\) and has type \(! (\top\rightarrow(\mathsf{qbit}\otimes\mathsf{qbit}))\) where \(\mathsf{qbit}\) is the base type of qubits. The \(\mathsf{nw}\) constant behaves like the new constant used in Section 2.3. \(\lambda_{sv}\)'s reductions are performed in a call-by-value setting. This is a central characteristic since different strategies are not equivalent (see the original paper or Reference [8]). Moreover, a mixed strategy can produce an hill-formed term. In Reference [43], the authors provide a categorical semantics for \(\lambda_{sv}\). For some recent investigations on semantic models, see Reference [44]. See also Reference [45], where the authors define a particle-style geometry of interaction [46] for \(\lambda_{sv}\). The pure quantum lambda calculus Q we employ in Example 1 is morally an heir of \(\lambda_{sv}\), despite the fact that it has been introduced for different scopes. In particular, the \"quantum Turing completeness\" (i.e., the equivalence with the Quantum Turing Machines) of Q has been proved, in joint with properties of the set of well forming rules (such as Subject Reduction) and a notion of _standardization_, that ideally aims to capture the separation between classical and quantum part of the computation.