We use the analogy between the quadrature operators in quantum optics and the phase-space coordinates in a mechanical harmonic oscillator to generalise the theory of linear optics beyond quantum theory. For this, we introduce a framework for analysing photonic circuits within generalised probabilistic theories based on quadrature operators. Using this framework, we ask whether phenomena like the Hong-Ou-Mandel effect, Mach-Zehnder interferometry are specific to quantum theory or also occur across a broader class of theories. We find the latter: the vanishing photon coincidences at the output of a beam splitter also occur for classical light and for a modified version of quantised light. Similarly, for Mach-Zehnder interferometry we find that there is no qualitative difference between quantum theory and these alternative theories. Our framework can serve as a foundation to study generalised theories of complex photonic set-ups and photonic quantum computers.
We use the analogy between the quadrature operators in quantum optics and the phase-space coordinates in a mechanical harmonic oscillator to generalise the theory of linear optics beyond quantum theory. For this, we introduce a framework for analysing photonic circuits within generalised probabilistic theories based on quadrature operators. Using this framework, we ask whether phenomena like the Hong-Ou-Mandel effect, Mach-Zehnder interferometry are specific to quantum theory or also occur across a broader class of theories. We find the latter: the vanishing photon coincidences at the output of a beam splitter also occur for classical light and for a modified version of quantised light. Similarly, for Mach-Zehnder interferometry we find that there is no qualitative difference between quantum theory and these alternative theories. Our framework can serve as a foundation to study generalised theories of complex photonic set-ups and photonic quantum computers.
This study explores how optical beam splitters provide a conceptual and operational link between classical and quantum descriptions of light. In the classical picture, they are modeled through energy-conserving field amplitudes and a four-port scattering matrix, which successfully explain interference in systems such as Michelson and Mach–Zehnder interferometers. Moving to the quantum domain, the field amplitudes are replaced by bosonic creation and annihilation operators that obey the Weyl–Heisenberg algebra. Using the Glauber displacement operator, we define coherent states whose expectation values reproduce classical monochromatic fields while exhibiting Poissonian photon statistics. This unified approach shows that beam splitters diagnose the nature of incident light: coherent states yield classical interference, while indistinguishable single-photons reveal quantum signatures such as antibunching and Hong–Ou–Mandel interference. The analysis relies on operator formalism and correlation functions that capture both average-field behavior and nonclassical statistics. As beam-splitting technologies transition from bulk optics to integrated photonics and metasurfaces, this framework offers a consistent basis for modeling optical circuits across the classical-quantum divide. By highlighting the dual role of the beam splitter as a passive device and a quantum probe, we emphasize its importance for quantum optics, quantum information, and hybrid photonic platforms.
At the beginning of the last century, the theory of quantum optics arose and led to a revolution in physics, since it allowed the interpretation of many unknown phenomena and the development of numerous powerful, cutting edge engineering applications, \nsuch as high precision laser technology. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation, numerical methods, computer algebra systems, and paper-and-pencil approaches are not well suited for quantum systems. In the last decade, a new emerging verification technique, called formal methods, became common among engineering domains, and has proven to be effective as an analysis tool. Formal methods \nconsist in the development of mathematical models of the system subject for analysis, and deriving computer-aided mathematical proofs. In this thesis, we propose a framework for the analysis of quantum optics based on formal methods, in particular theorem proving. The framework aims at implementing necessary quantum mechanics and optics concepts and theorems that facilitate the modelling of quantum optical devices and circuits, and then reason about them formally. To this end, the framework \nconsists of three major libraries: 1) Mathematical foundations, which mainly contain the theory of complex-valued-function linear spaces, 2) Quantum mechanics, which develops the general rules of quantum physics, and 3) Quantum Optics, which \nspecializes these rules for light beams and implements all related concepts, e.g., light coherence which is typically emitted by laser sources. On top of these theoretical foundations, we build a library of formal models of a number of optical devices commonly \nused in quantum circuits, including, beam splitters, light displacers, and light phase shifters. Using the proposed framework, we have been able to formally verify common quantum optical computing circuits, namely the Flip gate, CNOT gate, and Mach-Zehnder interferometer.
Phase lies at the heart of quantum physics and quantum information theory. A quantum bit is qualitatively different from a classical bit as it allows for the coherent superposition of possibilities, which demonstrate different behaviours depending on the phase between them. These behaviours constitute as interference phenomena, and lie behind the existence of algorithms in quantum computing which are arguably faster than the best classical alternatives. The concept of phase is deeply steeped in the structure of Hilbert spaces: the mathematical framework that underlies quantum theory. What if quantum theory did not hold in all scenarios, or was only a limiting case of some broader theory? In this case, would we still be able to meaningfully talk about phase and interference? In this thesis, we will adopt an operational generalisation of quantum theory known as the framework of generalised probabilistic theories. We will provide a reasonable definition of phase in this framework. Using this, we shall explore single-particle interferometry set-ups (particularly Mach-Zehnder interferometers): experiments whose output is highly dependent on the phase between the spatially disjoint branches through which a particle might be traversing. By applying physically-motivated locality considerations, we identify the crucial role that the uncertainty principle and its generalisations play in quantum theory as an enabler of non-trivial interference. By taking into account relativity of simultaneity, we will also provide a physical motivation for why standard quantum theory provides the best description of the location of a particle traversing such a system. Finally, we apply our generalised definition of phase in the related context of particle exchange behaviour, and identify a method for classifying post-quantum particles. All of this will demonstrate that phase between possibilities and its consequences are not uniquely quantum phenomena. Much of the behaviour we might ascribe to phase in quantum theory in fact holds generally true for phase in probabilistic theories.
Extending an existing quantum optic model for beamsplitters, a comprehensive model is developed from the first principles of quantum physics to describe photons traversing linear optical devices of arbitrary number of ports and even a circuit of devices, which are essential components of photonic quantum computing gates and circuits. The model derives the quantum operators and states of the photons at the egress ports of a device, gate or circuit from those at the ingress ports. As an application and validation, it is used to model the experiment that discovered the Hong-Ou-Mandel (HOM) effect and to explain the effect without the notion of quantum interference. The experiment is not only a landmark in the research of quantum optics but also important to photonic quantum computing design.
Grover multiports are higher-dimensional generalizations of beam splitters, in which input to any one of the four ports has equal probability of exiting at any of the same four ports, including the input port. In this paper, we demonstrate that interferometers built from such multiports have novel features. For example, when combined with two-photon input and coincidence measurements, it is shown that such interferometers have capabilities beyond those of standard beam-splitter-based interferometers, such as easily controlled interpolation between Hong-Ou-Mandel (HOM) and anti-HOM behavior. Further, it is shown that the Grover-based analog of the Mach-Zehnder interferometer can make three separate phase measurements simultaneously. By arranging the transmission lines between the two multiports to lie in different planes, the same interferometer acts as a higher-dimensional Sagnac interferometer, allowing rotation rates about three different axes to be measured with a single device.