A High Level Language for Monad-based Processes

编程中的副作用有多种形式和大小，例如本地和全局存储、异常、不确定性、恢复以及它们的多种组合。在编程语言的语义以及几种实际的编程语言(如Haskell和F#)中，使用Monad在类型系统中封装副作用是一种常见的做法。粗略地说，Monad是一种类型构造函数，它将一种类型的值转换为一种对这类值的计算产生副作用的类型，从而使副作用函数变成返回计算的纯函数。除了提供副作用范围的基于类型的描述之外，Monad很有吸引力，因为它们允许将Monad作为参数的泛型程序，然后可以实例化为所需的副作用概念；例如，在Haskell库中，这种参数化用于泛型循环构造。HighMoon的目标是推动基于Monad的程序的泛型元语言和验证逻辑的开发。在第二个项目阶段，我们的目标是在第一个项目阶段取得的基础成果的基础上，为同时产生副作用的过程提供通用的验证支持。在语义上，主要的研究对象是支持无保护迭代的Monad，即所谓的Elget Monad，以及捕获诸如恢复和进程间通信等反应性行为的操作。将这两个特征结合在一起的单体可以被视为具有反映单个计算步骤的净效果的外延级别和对反应性方面进行建模的内涵级别。关于Elget Monad的中心问题涉及到它们的代数的刻画和Elget Monad上的结构，从而允许系统地识别实例。我们将增强第一阶段开发的基于Monad的顺序程序的通用验证逻辑的表达能力和适用范围，并将其扩展到基于Monad的并发程序的通用验证逻辑。对于这样得到的逻辑，我们将开发(相对)完整的证明演算，以及适当限制片段的判定过程。

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.