Definition: Configuration

A configuration is $[\psi ,t]$, where $\psi$ is a unit vector in ${\mathcal{H}}_L$, modulo global phase, and $\mathrm{own}(t)=L$. It is well typed at $A$ if

Allocation extends the name-to-factor ordering by a fresh name; destructive readout restricts it to surviving names.