A High Level Language for Monad-based Processes

编程中的副作用有多种形式和大小，例如局部和全局存储、异常、非确定性、恢复以及它们的多重组合。在编程语言的语义以及一些实际的编程语言（如Haskell和f#）中，使用单子在类型系统中封装副作用是一种常见的做法。粗略地说，monad是一个类型构造函数，它将值的类型转换为此类值的副作用计算类型，从而使副作用函数变成返回计算的纯函数。除了提供基于类型的副作用范围描述外，单子还很有吸引力，因为它们允许将单子作为参数的泛型程序，然后可以实例化到期望的副作用概念；例如，在Haskell库中，这种参数化用于泛型循环构造。HighMoon的目标是为基于单子的程序推进通用元语言和验证逻辑的发展。在第二个项目阶段，我们的目标是在第一个项目阶段获得的基础结果的基础上，为并发的副作用过程提供一般的验证支持。从语义上讲，研究的主要对象是支持无保护迭代的单子，即所谓的Elgot单子，它与捕获反应性行为（如恢复和进程间通信）的操作相结合。结合这两个特性的单子可以被看作具有外延级，反映单个计算步骤的净效果，而具有内延级，对响应方面进行建模。关于Elgot单子的中心问题涉及它们的代数特征和Elgot单子上的结构，允许系统地识别例子。我们将增强在第一个项目阶段开发的基于顺序单子的程序的通用验证逻辑，考虑到它们的表现力和适用性范围，并将它们扩展到基于单子的并发程序的通用验证逻辑。对于由此获得的逻辑，我们将开发（相对）完整的证明演算，以及适当限制片段的决策程序。

Side-effects in programming come in many shapes and sizes, such as local and global store, exceptions, non-determinism, resumptions, and manyfold combinations thereof. In the semantics of programming languages as well as in several actual programming languages, such as Haskell and F#, it is common practice to encapsulate side-effects in the type system using monads. Roughly, a monad is a type constructor that turns a type of values into a type of side-effecting computations of such values, so that a side-effecting function becomes a pure function that returns a computation. Besides affording a type-based delineation of the scope of side-effects, monads are attractive because they allow for generic programs that take the monad as a parameter, and then can be instantiated to the desired notion of side-effect; e.g. in the Haskell library, this parametrization is used for generic loop constructs.The goal of HighMoon is to advance the development of generic metalanguages and verification logics for monad-based programs. In the second project phase, we aim to provide generic verification support for concurrent side-effecting processes, building on foundational results obtained in the first project phase. Semantically, the main object of study are monads that support unguarded iteration, so-called Elgot monads, in combination with operations that capture reactive behaviour such as resumptions and inter-process communication. Monads combining these two features may be seen as having an extensional level, reflecting the net effect of individual computation steps, and an intensional one that models reactive aspects. Central questions on Elgot monads concern the characterization of their algebras and constructions on Elgot monads that allow for the systematic identification of examples. We will enhance the generic verification logics for sequential monad-based programs developed in the first project phase with respect to both their expressivity and their range of applicability, and extend them to generic verification logics for monad-based concurrent programs. For the logics thus obtained, we will develop (relatively) complete proof calculi, as well as decision procedures for suitably restricted fragments.