One of the purposes of quantum programming languages is to express quantum programs, however a possibly more important reason is to provide a framework for reasoning about the programs expressing quantum algorithms -- and hence about quantum computation in general.
Indeed, in classical computer science it is frequent to express the reasoning behind a program via several formally-defined logics. These logics provide important frameworks in which to reason and prove properties about the computational processes. Often they arise via the study of type systems for the language. Related to our motivation there is already a quantum logic, which was developed before quantum computing, and which is not known to have a clear relation to quantum programs and algorithms.
The Linear-Algebraic Lambda-Calculus extends the Lambda-Calculus with the possibility to make arbitrary linear combinations of terms a.t+b.u. We want to set up a type system for it which is capable of such handling vectorial notions, i.e. were types themselves form a vector space. This is needed at a practical level for instance in order to prove normalization and unitarity properties of terms. There is also the intriguing question as to what logical meaning we can give these `superposition types'.
Joint work with Pablo Arrighi.