A High Level Language for Monad-based Processes

点击翻译按钮获取中文摘要

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.