In this work in progress, we describe a new logic and type system for higher order quantum operations, derived from linear logic. It features two tiers of formulae, separating ground quantum data and higher order types, and presents a new connective $\rightleftharpoons$ for unitaries.

Soundess of unitaries is achieved by introducing worlds to a section of the sequent calculus, allowing us to discriminate cases and treat them differently, and still merge them into a single output case that respects unitarity.

We prove that the semantics given to this logic are sound, can encode known higher order quantum operation, and are consistent with routed circuits, an existing language for order two quantum operations.