Proof Nets for Quantum Computing

May 12, 2025

Kostia Chardonnet (INRIA Nancy)

Most models of quantum computing do not allow to represent efficiently “quantum control flow” : the possibility to have a quantum superposition between two different executions.
For instance, the quantum program “if x then P1 else P2” can be understood as a superposition of both P1 and P2 being executed at the same time.
In this talk, we explore how the additive structure of linear logic can be used to model quantum control flow. To this end, we introduce the “Many-Worlds Calculus”, a graphical language based on the Multiplicative Additive Proof Nets of Linear Logic for quantum computing. The graphical language comes equipped with a denotational semantics based on linear maps, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.