Causality in Pure Quantum Computation with Quantum Control

Abstract:Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

Full version of the conference paper at LICS 2026. 34 pages

Programming Languages (cs.PL); Logic in Computer Science (cs.LO); Quantum Physics (quant-ph)

arXiv:2607.15926 [cs.PL]

(or arXiv:2607.15926v1 [cs.PL] for this version)

https://doi.org/10.48550/arXiv.2607.15926 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

https://doi.org/10.4230/LIPIcs.LICS.2026.57 Focus to learn more DOI(s) linking to related resources

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.