Effects and algebraic theories.

该项目福尔斯属于EPSRC信息和通信技术（ICT）的研究主题。该项目涉及编程语言的基础，它们的语义和类型系统。计算效果是编程语言的一个特征，代表不纯粹的行为，例如输入和输出操作、异常、状态、不确定性。这些操作在实际编程中被广泛使用，并且由许多编程语言提供。然而，它们的数学基础还没有得到充分的探讨，在他的有影响力的工作，莫吉给出了一个一般的指称语义计算效果使用单子。他的想法随后被Haskell用纯函数语言实现，其中monad被用来模拟副作用。Plotkin和Power引入了代数效应的概念，这是一种计算效应的特殊方法，其中不纯的行为来自一组操作。这些操作的属性由方程指定，使得有可能将代数效应作为代数理论来呈现，传统上在泛代数中进行研究。每一个代数理论都产生一个单子，从而展示了与莫吉语义学的联系。为了解释效果，一阶代数理论的各种扩展已经被提出。例子包括Staton提出的参数化代数理论，以及Fiore，Hur和Mahmoud开发的二阶代数理论。Fiore和Staton使用替代代数和右lambda代数，二阶代数理论的特殊实例，分别对跳跃效应和涉及代码指针堆栈的计算进行建模。进一步探索效应和二阶代数理论之间的联系是我将追求的一个有前途的研究方向。我们的目标是找到其他代数理论，产生的影响，反之亦然。首先，这种方法将导致更好地理解效果的语义。从长远来看，效果和代数之间的联系可以为扩展具有计算效果的编程演算提供一个通用框架。这些扩展可以在高级通用编程语言之上实现。在ICT研究主题中，该项目是理论计算机科学领域的一部分，因为它采用了形式推理，逻辑概念和语义。该项目也是编程语言和编译器领域的一部分，因为它的目的是更好地理解编程语言，并可能导致新的实现。

This project falls within the EPSRC Information and communication technologies (ICT) research theme.This project is concerned with the foundations of programming languages, their semantics and type systems. Computational effects are a feature of programming languages representing impure behaviour, such as input and output operations, exceptions, state, nondeterminism. These operations are widely used in practical programming and are provided by many programming languages. However, their mathematical foundations have not been fully explored yet.In his influential work, Moggi gives a general denotational semantics for computational effects using monads. His idea was subsequently implemented in the pure functional language by Haskell, where monads are used to simulate side effects. Plotkin and Power introduce the idea of algebraic effects, a particular approach to computational effects where the impure behaviour results from a set of operations. The properties of these operations are specified by equations, making it possible to present algebraic effects as algebraic theories, traditionally studied in universal algebra. Each algebraic theory gives rise to a monad, thus exhibiting the connection with Moggi's semantics.In order to interpret effects, various extensions of first-order algebraic theories have been proposed. Examples include parameterised algebraic theories, proposed by Staton, and second-order algebraic theories developed by Fiore, Hur and Mahmoud. Fiore and Staton use substitution algebras and right lambda algebras, particular instances of second-order algebraic theories, to model jump effects and computation involving stacks of code pointers, respectively.Exploring further the connection between effects and second-order algebraic theories is a promising research direction that I will pursue. The goal is to find other algebraic theories that give rise to effects and vice-versa. In the first instance, this approach will lead to a better understanding of the semantics of effects. In the long term, the connection between effects and algebra could provide a general framework for extending programming calculi with computational effects. These extensions could then be implemented on top of high-level general-purpose programming languages. Within the ICT research theme, this project is part of the Theoretical Computer Science area because it employs formal reasoning, logical concepts and semantics. The project is also part of the Programming languages and compilers area since its aim is to understand programming languages better, and may lead to new implementations.