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.

翻译：本论文围绕计算机科学中称为"语义学"的领域展开研究，主要涉及操作语义、等式理论与指称语义。论文的第一项贡献是通过单子（monad）的棱镜研究效应的交换性。单子是幺半群等代数结构的推广，这些结构具有中心的概念：幺半群的中心由与所有其他元素可交换的元素构成。我们给出了单子存在中心的充分必要条件，并详细阐述了携带效应中心性信息的语言语义。此外，我们建立了该语言等式理论与指称语义之间的紧密联系。论文的第二部分聚焦于被视为可逆效应的量子计算。物理上允许的量子操作除测量外皆可逆；然而测量可推迟至计算末尾，使我们能先专注于可逆部分。我们定义了一种执行量子操作（称为"酉变换"）的简单类型化可逆编程语言，提出了适用于该语言的指称语义与等式理论，并证明了前者的完备性。进一步地，我们研究了可逆编程中的递归问题，为图灵完备的可逆函数式编程语言提供了适当的操作语义与指称语义，其中指称语义采用rig并逆范畴的dcpo富化方法。这种关于可逆计算高阶推理的数学描述不能直接推广到量子计算情形。在结论部分，我们详细阐述了通过受保护递归实现高阶量子控制的局限性与未来可能方向。