# Quantum Calculi--From Theory to Language Design
## 3 Quantum Programming Languages  
In recent years, we have seen an increase in quantum software platforms. Mainstream industries, such as IBM and Microsoft, invested a huge amount of resources both in software development and in the technological advance.  
The world of quantum programming can claim two decades of interesting research and is growing day-by-day. In this section, we only focus on a fragment of this world and remand to the literature for a complete overview. Quantum languages can be divided into three classes: practical-minded tools for generating quantum circuit description; quantum languages with a limited (or still underdeveloped) theoretical account; theoretically attractive languages with a focus on semantics and denotational models.  
To the first category belongs **Forest**, the quantum software platform developed by [PERSON] and **Qiskit** (**Quantum Information Software Kit**), an opensource platform developed by IBM for the 20-qubits quantum computer _IBM Q Experience_. **Forest** includes an opensource quantum language called PyQuil embedded in Pylon and offers to the user both a small online real quantum architecture named Quantum Processing Unit (QPU) that support computations up to 8 qubits and a remote Quantum Virtual Machine (QVM) for simulation up to 30 qubits. **Qiskit** native language is OpenQASM, a low-level quantum assembly language that provides instruction to the actual quantum devices, similarly to PyQuil. IBM provides local and cloud-based quantum simulators (up to 25 qubits). For a complete account and comparison of open-source quantum programming platforms, see Reference [1].  
The second category hosts languages such as Quipper by [PERSON], [PERSON] et al. [42] and the **Quantum developers KIT**, based on the language Q# by Microsoft. Quipper represents one of the more advanced academic reality in the landscape of quantum languages. Quipper represents one of the more advanced academic reality in the landscape of quantum languages. Quipper is embedded (an embedded language provide a \"quantum core\" sophistically interfaced with a host \"classical\" language) in Haskell and is based on the QRAM model, successively rephrased in terms of _quantum co-processors_ in Reference [23]. Quipper is higher-order, scalable, permits to easily write programs using ancillae qubits [9], allows to compile classical programs into quantum circuits and simulate in Haskell quantum computations. Moreover, the language pursues the goal to optimize the number of resources needed for computations. Also to this end, in Quipper a neat separation between compile-time inputs (called _parameters_) and run-time inputs (sometimes called _states_) is explicit. Quipper does not have a dedicated type system and so lacks both linear and dependent types (see Section 2.3) and does not support a denotational semantics. For this reason, in the present survey, we will focus only on a class of Quipper sub-languages called Proto - Quipper.  
Q#, recently introduced by Microsoft, is a stand-alone (i.e., non-embedded) domain-specific programming language used for expressing quantum algorithms. It allows us to write sub-programs that execute on an adjunct quantum processor under the control of a classical host program (in this sense, Q# is a QRAM based language) and also includes a resource estimator. Literature about theoretical properties of Q# is still missing. Despite some feature such as the use of polymorphic types being very interesting, in this paper we do not go deeper in the discussion and remand to the on-line documentation [25].  
The third category is the one we focus on in Section 4.