The Semantics of Effects: Centrality, Quantum Control and Reversible Recursion
Louis Lemonnier
TL;DR
The thesis develops a rigorous, category-theoretic account of semantics for programming languages with effects, focusing on the centre of strong monads, central submonads, and their internal languages, then applies these ideas to quantum control and reversible recursion. It introduces a Central Submonad Calculus (CSC) that separates central from non-central effects, provides soundness and completeness results with respect to CSC-models, and establishes an internal-language correspondence. A second pillar treats quantum computing as a reversible algebraic effect, presenting a simply-typed reversible language for unitary quantum operations with a complete denotational semantics, and a complementary study of recursion in reversible (and guard-checked) quantum contexts. Together, the work lays foundational, high-order semantic tools for reasoning about effects and quantum-control in programming languages, highlighting both the potential and limits of higher-order quantum control. It also clarifies how centres and central submonads interact with monadic structure, premongular centers, and Lawvere theories, offering a robust framework for future extensions to commutants, distributive laws, and guarded recursion in quantum settings.
Abstract
This thesis revolves around an area of computer science called "semantics". We work with operational semantics, equational theories, and denotational semantics. The first contribution of this thesis is a study of the commutativity of effects through the prism of monads. Monads are the generalisation of algebraic structures such as monoids, which have a notion of centre: the centre of a monoid is made of elements which commute with all others. We provide the necessary and sufficient conditions for a monad to have a centre. We also detail the semantics of a language with effects that carry information on which effects are central. Moreover, we provide a strong link between its equational theories and its denotational semantics. The second focus of the thesis is quantum computing, seen as a reversible effect. Physically permissible quantum operations are all reversible, except measurement; however, measurement can be deferred at the end of the computation, allowing us to focus on the reversible part first. We define a simply-typed reversible programming language performing quantum operations called "unitaries". A denotational semantics and an equational theory adapted to the language are presented, and we prove that the former is complete. Furthermore, we study recursion in reversible programming, providing adequate operational and denotational semantics to a Turing-complete, reversible, functional programming language. The denotational semantics uses the dcpo enrichment of rig join inverse categories. This mathematical account of higher-order reasoning on reversible computing does not directly generalise to its quantum counterpart. In the conclusion, we detail the limitations and possible future for higher-order quantum control through guarded recursion.