Types and terms

Types are

Tensor powers are right nested: $A^{\otimes 0}=1$ and $A^{\otimes 1}=A$. The empty tuple is $\ast$. Linear pairing and elimination implement the usual associativity and unit isomorphisms. Tuple notation suppresses these administrative maps, not resource uses.

Terms are

Source variables are $x,y,\dots$. Runtime names $q,r,\dots$ are introduced by allocation. Source programs contain no runtime names. Every finite-register unitary is available as a gate; a dense-gate variant is given in Corollary cor:dense.

We abbreviate $(\lambda x:A.u)t$ by $\mathsf{let}x=t\mathsf{in}u$. Tuple-pattern binders abbreviate iterated linear tuple elimination.