This tutorial will present a low-level operational model for higher-order quantum computation, using Geometry of Interaction as framework. The plan of the the session is a follows. In a first part, we shall see what is quantum computation, and how a suitably typed quantum lambda-calculus can relate to linear logic. In a second independent part, we shall recap what is a proof-net, and describe the two operational semantics on proof-nets relevant to this talk: the first one using graph rewriting, the other using tokens flowing in the graph (aka what we call Geometry of Interaction). In the third and last part of the talk, we shall discuss how to merge the two constructions, to see how to get a quantum Geometry of Interaction. The construction is modular: we shall see how to add probabilistic behavior to proof-nets, how to augment them with registers, and how to deal with the synchronization required for quantum computation. If time permits, we'll discuss an algebraic presentation of memory using nominal sets that is amenable to other computational models.

This presentation will assume basic knowledge of

• sequent calculus
• lambda-calculus
• linear logic
• (some) notion of linear algebra