  While much of the current study on quantum computation employs low-level
formalisms such as quantum circuits, several high-level languages/calculi have
been recently proposed aiming at structured quantum programming. The current
work contributes to the semantical study of such languages by providing
interaction-based semantics of a functional quantum programming language; the
latter is, much like Selinger and Valiron's, based on linear lambda calculus
and equipped with features like the ! modality and recursion. The proposed
denotational model is the first one that supports the full features of a
quantum functional programming language; we prove adequacy of our semantics.
The construction of our model is by a series of existing techniques taken from
the semantics of classical computation as well as from process theory. The most
notable among them is Girard's Geometry of Interaction (GoI), categorically
formulated by Abramsky, Haghverdi and Scott. The mathematical genericity of
these techniques---largely due to their categorical formulation---is exploited
for our move from classical to quantum.
