Coinductive Techniques on a Linear Quantum λ-Calculus

In this thesis, it is examined the issue of equivalence between linear terms in higher order languages, that is, in languages which allow to use functions as variables, and where variables which appear in the terms must be used exactly once. The work is developed focusing on the bisimulation method, with the purpose to compare this technique with that which has become the standard for the comparison between the terms of a language, i.e. the context equivalence. The thesis is divided into three parts: in the first one, the introduction of the bisimulation and context equivalence techniques takes place within a deterministic linear and typed language. In the second part, the same techniques are reformulated for a language that, while preserving the linearity, loses the deterministic connotation, allowing the terms to evaluate to a set of values each one having a certain probability to appear in the end of calculation. In the last part, a quantum language is examined, discussing the advantages of quantum computation, which allows to speed-up many of the algorithms of computation. Here one gives the concept of quantum program, which is inextricably linked to the (quantum) register where the qubits used in the computation are stored, entailing a more complex notion of equivalence between terms. The techniques to demonstrate that bisimulation is a congruence are not standard and have been used for the first time by Howe for untyped languages: within the thesis, one shows that bisimulation is a congruence in all considered languages but it coincides with the context equivalence relation only for the deterministic one. Indeed, extending the techniques already used by Howe to the probabilistic and quantum environment, it is shown, as non trivial result, that in probabilistic and quantum linear languages the bisimulation is contained in context equivalence relation.