This thesis explores both theoretical and practical aspects of concurrent programming languages that integrate probabilistic and/or quantum computations. On the theoretical side, we investigate how event structures, a model for concurrency, can be used to furnish concurrent languages with denotational semantics. Event structures are studied in three distinct settings: non-deterministic, probabilistic, and quantum computation. Based on these three realms, we successively extend a core imperative-like concurrent language with non-deterministic choice, probabilistic choice, and standard quantum operations. For each extension, we define both operational and denotational semantics and establish their equivalence through soundness and adequacy results. Soundness ensures that every behavior obtainable through the operational semantics is reflected denotationally, showing that the denotational semantics correctly abstracts the computations. Conversely, adequacy guarantees that whenever the denotational semantics yields a value, this value can be produced by the operational semantics, demonstrating that the operational semantics explicitly realises what the denotational semantics predicts. On the practical side, motivated by the growing interplay between classical and quantum computers, we integrate non-deterministic choice, probabilistic choice, and quantum operations into a single language, further extended with a synchronization primitive. We develop an interpreter for this language and test it on several illustrative examples, including three versions of the Dining Philosophers problem: concurrentonly, probabilistic, and quantum. Using our tool, we demonstrate that a result stated in the literature about the quantum Dining Philosophers problem does not hold, leaving open the question of whether an efficient algorithm for solving it exists.
This thesis explores both theoretical and practical aspects of concurrent programming languages that integrate probabilistic and/or quantum computations. On the theoretical side, we investigate how event structures, a model for concurrency, can be used to furnish concurrent languages with denotational semantics. Event structures are studied in three distinct settings: non-deterministic, probabilistic, and quantum computation. Based on these three realms, we successively extend a core imperative-like concurrent language with non-deterministic choice, probabilistic choice, and standard quantum operations. For each extension, we define both operational and denotational semantics and establish their equivalence through soundness and adequacy results. Soundness ensures that every behavior obtainable through the operational semantics is reflected denotationally, showing that the denotational semantics correctly abstracts the computations. Conversely, adequacy guarantees that whenever the denotational semantics yields a value, this value can be produced by the operational semantics, demonstrating that the operational semantics explicitly realises what the denotational semantics predicts. On the practical side, motivated by the growing interplay between classical and quantum computers, we integrate non-deterministic choice, probabilistic choice, and quantum operations into a single language, further extended with a synchronization primitive. We develop an interpreter for this language and test it on several illustrative examples, including three versions of the Dining Philosophers problem: concurrentonly, probabilistic, and quantum. Using our tool, we demonstrate that a result stated in the literature about the quantum Dining Philosophers problem does not hold, leaving open the question of whether an efficient algorithm for solving it exists.
The development of Quantum Communication Protocols sparked the interest in quantum extensions of process calculi. However, existing semantic models, typically based on probability distributions and probabilistic transition systems, often fail to adequately capture the nuances of Quantum Mechanics. They can spuriously distinguish between systems that quantum theory deems identical, and allow for physically unfeasible non-deterministic capabilities. Furthermore, their reliance on concrete quantum states makes automated verification computationally intractable due to the infinite, continuous nature of the state space. To overcome these challenges, this thesis proposes to model quantum protocols in a novel manner, by leveraging both the mathematical language of Quantum Theory and the verification techniques of Computer Science. The main objective is to develop a verification framework that is both physically sound and amenable to symbolic, tractable analysis. This is achieved through the development of two novel models of quantum concurrent systems. The first major contribution is a new semantic model that respects quantum indistinguishability by construction. Quantum theory teaches us that probabilistic mixtures of quantum states should not be modelled as probability distributions. We thus introduce Density Distributions, where processes are weighted by density operators rather than scalar probabilities. We define an operational semantics based on these distributions and introduce Quantum Labelled Bisimilarity, the first behavioural equivalence to be a congruence under physically admissible scheduling policies. We show that our equivalence coincides with a purely observational, context-based, saturated bisimilarity, thus proving its adequacy in terms of discriminating power. The second core contribution is an elementary framework for the symbolic verification of quantum protocols. To abstract away from concrete quantum inputs, we develop a mathematical theory of Conditional Quantum Effects, a novel generalization of quantum effects capable of representing conditional probabilities arising from quantum measurements. Building on this foundation, we define Effect-weighted Labelled Transition Systems (eLTSs), an input-independent model for concurrent quantum systems. We propose a "Heisenberg-style" symbolic semantics that maps any quantum protocol to a single eLTS. We prove that symbolic bisimilarity on these eLTSs is fully abstract with respect to ground probabilistic bisimilarity: two symbolic systems are equivalent if and only if they yield equivalent pLTSs under all possible quantum inputs.
In this thesis, we study quantum programming languages, and focus on the quantum lambda-calculus, a paradigmatic language defined by Selinger and Valiron, which mixes a rich classical control flow (higher order functions, etc.) and quantum data (qubit creation, measure, and unitary operations). In this thesis, we search for a denotational semantics of this language, in other words, we extract the meaning and behaviour of programs by interpreting them in an adequately chosen mathematical universe. In order to model the quantum lambda-calculus, one must adapt the traditional denotational models to the mathematics of quantum computation (Hilbert spaces, density matrices, etc.). We have three main contributions:Firstly, we extend game semantics to the quantum case. Game semantics is a dynamic approach to denotational semantics, which focuses on the sequence of interactions between a program and its environment. We obtain the first denotational model of the full quantum lambda-calculus which is both compositional and interactive, meaning that it represents the dynamic of the execution. Our model generalise the recently developed model for the probabilistic case.Secondly, we formally link our model to the only pre-existing denotational model of the full lambda-calculus, the quantum relational model of Pagani, Selinger and Valiron.Lastly, we prove that our game model is fully abstract, the gold standard of denotational semantics, which ensures a total correspondence between the programming language and the model. We deduce that the quantum relational model was also fully abstract, which was an open problem.This thesis is constituted of three parts. The first part details some preliminaries on category theory, used for defining a formal framework including both the quantum game model and the quantum relational model, some preliminaries on the mathematics of quantum computation, and then some preliminaries on quantum programming and its models. The second part starts with some preliminaries on game semantics and defines our quantum game model in the simplified case of the linear quantum lambda-calculus. The third part builds on the second part to define the full quantum game model, prove its full abstraction, and deduce that the quantum relational model is fully abstract too.
This thesis focuses on two different aspects of quantum computation: quantum complexity and quantum semantics. In the first part, I study the quantum complexity mainly within the quantum query model. Together with my colleagues, I introduce a new framework for quantum query complexity, phrased in terms of the minimal oracle and analyse limits and strengths of this new model in comparison to their classical and quantum counterparts. Working within the query model I study quantum one-way functions. I show that in the quantum setting, the problem of the existence of a quantum one-way permutation can be reduced to the problem of constructing polynomial size networks for performing the specific task of the reflection about a sequence of states. Furthermore, I extend these results to the domain of the state and operator complexity. I show that if a quantum one-way function exists, then we can construct a sequence of so called “hard” states with the property that the reflection operators about those states are efficiently implementable. In the second part, I study the extension of domain theory to the quantum setting and develop the semantics of quantum computation. By defining a quantum domain I introduce a rigourous definition of quantum computability for quantum states and operators. Furthermore I show that the denotational semantics of quantum computation has the same semantical structure as the denotational semantics of classical probabilistic computation introduced by Kozen. This could be considered as a foundation for designing functional programming languages for quantum computation. Finally, I continue with an abstract mathematical approach to study a general formalism for describing entanglement manipulation and introduce a new approach to derive a unique measure of entanglement for bipartite quantum pure states.
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.
Quantum programming introduces both probabilistic and non-deterministic behavior, making formal verification a challenging task. This work develops a framework for modeling non-deterministic quantum programs using Markov Decision Processes (MDPs). Each program configuration is represented as a combination of the remaining program and its quantum state, while transitions capture both quantum evolution and non-deterministic branching. We define operational semantics for quantum programs in terms of MDPs and prove their equivalence to established denotational semantics. This equivalence ensures consistency between high-level mathematical descriptions and executable models. The approach enables the application of model-checking techniques, originally designed for classical probabilistic systems, to quantum programs. Our results show that MDPs provide a foundation for verifying properties of non-deterministic quantum programs.
The objective of this thesis is to develop a semantics for higher-order quantum information. Following the work done in the author's M.Sc. thesis, we study a lambda calculus for quantum computation with classical control. The language features two important properties. The first one, arising from the so-called no-cloning theorem of quantum computation, is the need for a distinction between duplicable and non-duplicable elements. For keeping track of duplicability at higher order, we use a type system inspired by the resource-sensitive linear logic. The second important aspect is the probability inherent to measurement, the only operation for retrieving classical data from quantum data. This forces us into choosing a reduction strategy for being able to define an operational semantics. We address the question of a denotational semantics in two respects. First, we restrict the study to the strictly linear aspect of the language. Doing so, we suppress the need for distinguishing between duplicable and non-duplicable elements and we can focus on the description of quantum features at higher order. Using the category of completely positive maps as a framework, we build a fully abstract denotational model of the strictly linear fragment of the language. The study of the full language is more demanding. For dealing with the probabilistic aspect of the language, we use a method inspired by Moggi and build a computational model with a distinction between values and computations. For the distinction between duplicability and non-duplicability in the calculus, we adapt Bierman's linear category, where the duplication is considered as a comonad with specific properties. The resulting model is what we call a linear category for duplication. Finally, we only focus on the fragment of the language that contains the aforementioned elements, and remove the classical Boolean and quantum Boolean features to get a generic computational linear lambda-calculus. In this idealized setting, we show that such a language have a full and complete interpretation in a linear category for duplication.