Assumption: Finite compositional program interface

A selected calculus has well-typed finite first-order quantum and classical interfaces. It supports sequential composition, tensor composition on disjoint owned interfaces, finite classical control, allocation, its declared gate library, and destructive readout.

The denotation of a composite program is the corresponding composition of complete instruments. Every selected local generating program terminates and has a strategy-independent denotation. Programs and controllers do not inspect a description of the unknown quantum state.