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.