**Third party funded individual grant**

**Acronym:**
HighMoon/HighMoon2

**Start date :**
01.09.2013

**End date :**
31.10.2020

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.

In the analysis of programs, side-effects are notoriously problematic as they induce a gap between programs and the mathematical notion of function. A well-established approach to this issue is to encapsulate side-effects as monads, which lift types of values to types of computations — thus, sideeffecting functions become pure functions returning computations. Technically, this paradigm, as used in functional languages such as Haskell or F#, is based on Moggi’s computational metalanguage. However, the computational metalanguage and generic program logics based on it are currently limited to sequential programming over comparatively simple memory models. Contrastingly, specialized program logics and practical monad-based programming nowadays encompass advanced features such as concurrency and heap separation. Our aim is to provide the foundations of a unified framework to support the next generation of monad-based programming principles and program logics. To this end, we will extend the computational metalanguage, which works within a fixed single effect, to a High Level Monadic Metalanguage (HMML) which lives over the category of monads and hence accommodates morphisms and standard constructions of monads. The HMML will be equipped with interactive and, where possible, automatic reasoning support. Within the HMML, we will develop generic programming constructs and program logics for side-effecting concurrent processes and heap separation.