We establish a formal bridge between qubit-based and photonic quantum computing. We do this by defining a functor from the ZX calculus to linear optical circuits. In the process we provide a compositional theory of quantum linear optics which allows to reason about events involving multiple photons such as those required to perform linear-optical and fusion-based quantum computing.
We establish a formal bridge between qubit-based and photonic quantum computing. We do this by defining a functor from the ZX calculus to linear optical circuits. In the process we provide a compositional theory of quantum linear optics which allows to reason about events involving multiple photons such as those required to perform linear-optical and fusion-based quantum computing.
Photonic systems offer a promising platform for interconnecting quantum processors and enabling scalable, networked architectures. Designing and verifying such architectures requires a unified formalism that integrates linear algebraic reasoning with probabilistic and control-flow structures. In this work, we introduce a graphical framework for distributed quantum computing that brings together linear optics, the ZX-calculus, and dataflow programming. Our language supports the formal analysis and optimization of distributed protocols involving both qubits and photonic modes, with explicit interfaces for classical control and feedforward, all expressed within a synchronous dataflow model with discrete-time dynamics. Within this setting, we classify entangling photonic fusion measurements, show how their induced Pauli errors can be corrected via a novel flow structure for fusion networks, and establish correctness proofs for new repeat-until-success protocols enabling arbitrary fusions. Layer by layer, we construct qubit architectures incorporating practical optical components such as beam splitters, switches, and photon sources, with graphical proofs that they are deterministic and support universal quantum computation. Together, these results establish a foundation for verifiable compilation and automated optimization in networked quantum computing.
Entangled dual-rail photonic qubit states are important resource states for measurement-based and fusion-based quantum computing. However, their generation is highly challenging due to the probabilistic nature of entangling operations. Here, the authors introduce a formalism using ZX diagrams to design linear optical systems that can generate entangled multiqubit states of dual-rail photonic qubits. This formalism makes it easier to compare methods for creating a desired photonic state and to find the most optimal one.
Photonics offers a promising platform for implementations of measurement-based quantum computing. Recently proposed fusion-based architectures aim to achieve universality and fault-tolerance. In these approaches, computation is carried out by performing fusion and single-qubit measurements on a resource graph state. The verification of these architectures requires linear algebraic, probabilistic, and control flow structures to be combined in a unified formal language. This paper develops a framework for photonic quantum computing by bringing together linear optics, ZX calculus, and dataflow programming. We characterize fusion measurements that induce Pauli errors and show that they are correctable using a novel flow structure for fusion networks. We prove the correctness of new repeat-until-success protocols for the realization of arbitrary fusions and provide a graph-theoretic proof of universality for linear optics with entangled photon sources. The proposed framework paves the way for the development of compilation algorithms for photonic quantum computing.
In the models of quantum computing usually considered, some quantum data is manipulated by means of operations which are controlled in an essentially classical way. Controlling these operations in a quantum way is actually possible, but has been much less studied. In particular, quantum control misses a formalism in which one could represent it in a simple way in order to efficiently reason on processes involving it. The first contribution of this thesis is to lay the foundations of a formal framework dedicated to quantum control, in the form of a graphical language. Our main result about this language is the introduction of a complete equational theory, that is, a set of equations that makes it possible, by successive local rewriting, to transform a given diagram into any other diagram representing the same program or physical process. A second contribution is to apply this formalism, on the one hand, to the problem of resource optimisation of processes involving quantum control, and on the other hand, to the characterisation of the observational equivalence of quantum communication channels. A third contribution of this thesis is to introduce a language for linear optical circuits. We equip this language with a complete equational theory, together with a simple normal form, reachable via a strongly normalising and confluent rewriting system. The last contribution of this thesis, maybe the most significant one, is to introduce a complete equational theory for the language of quantum circuits. We obtain this result by exploiting a correspondence between quantum circuits and optical circuits, which allows us to transfer the equational theory already obtained for optical circuits.
The ZX-calculus is a graphical language for reasoning about quantum computation that has recently seen an increased usage in a variety of areas such as quantum circuit optimisation, surface codes and lattice surgery, measurement-based quantum computation, and quantum foundations. The first half of this review gives a gentle introduction to the ZX-calculus suitable for those familiar with the basics of quantum computing. The aim here is to make the reader comfortable enough with the ZX-calculus that they could use it in their daily work for small computations on quantum circuits and states. The latter sections give a condensed overview of the literature on the ZX-calculus. We discuss Clifford computation and graphically prove the Gottesman-Knill theorem, we discuss a recently introduced extension of the ZX-calculus that allows for convenient reasoning about Toffoli gates, and we discuss the recent completeness theorems for the ZX-calculus that show that, in principle, all reasoning about quantum computation can be done using ZX-diagrams. Additionally, we discuss the categorical and algebraic origins of the ZX-calculus and we discuss several extensions of the language which can represent mixed states, measurement, classical control and higher-dimensional qudits.
We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.