New Programming Language Enforces Causality in Quantum Programs

Kengo Hirata and Takeshi Tsukada are developing a new programming language to address a fundamental question in quantum computing: what separates physically possible processes from those that remain theoretical. They have proposed a “typed lambda calculus with quantum control” designed to enforce causality, extending existing quantum computation with higher-order functions and quantum conditional branching. The work stems from a distinction between an example called the quantum SWITCH, for which implementations have been proposed, and an example called the OCB process, which is suspected to be unrealizable; this contrast is driving the investigation into the limits of quantum mechanics. According to the paper, “Not all such processes are believed to be physically realizable,” and the researchers are studying whether unrealizable processes are undefinable within their formally defined system, built on intuitionistic BV logic and a model related to the Caus construction.

The distinction between quantum processes considered physically possible and those that are not hinges on the realizability of specific implementations. While the quantum SWITCH has been proposed as a viable design, the “OCB process” remains suspect. This is not merely theoretical exploration; the researchers are studying whether processes deemed physically unrealizable are definable within the constraints of their newly developed language. The paper details a categorical semantics for this calculus, offering a rigorous framework to analyze and constrain quantum operations. The full paper, presented at LICS 2026, comprises 34 pages and demonstrates a commitment to formal verification, suggesting a future where quantum program correctness is provable through logical means, rather than relying solely on empirical observation. This approach could be crucial for building reliable and predictable quantum technologies.