A High Level Language for Monad-based Processes

Third party funded individual grant

Project Details

Project leader:
Prof. Dr. Lutz Schröder
PD Dr.-Ing. Sergey Goncharov

Contributing FAU Organisations:
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Technische Fakultät

Funding source: DFG-Einzelförderung / Sachbeihilfe (EIN-SBH)
Acronym: HighMoon2
Start date: 01/11/2017
End date: 31/10/2020

Short description (intelligible to all):

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.


Goncharov, S., & Schröder, L. (2018). Guarded Traced Categories. (pp. 313-330). Springer Verlag.
Goncharov, S., Schröder, L., Rauch, C., & Jakob, J. (2018). Unguarded Recursion on Coinductive Resumptions. Logical Methods in Computer Science, 14(3). https://dx.doi.org/10.23638/LMCS-14(3:10)2018
Rauch, C., Goncharov, S., & Schröder, L. (2017). Generic Hoare Logic for Order-Enriched Effects with Exceptions. In James P, Roggenbach M (Eds.), Recent Trends in Algebraic Development Techniques: 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers (pp. 208--222). Springer.
Goncharov, S., Schröder, L., Rauch, C., & Piróg, M. (2017). Unifying Guarded and Unguarded Iteration. In Esparza Javier , Murawski Andrzej (Eds.), Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017). Uppsala, SE: Berlin: Springer.

Last updated on 2018-05-09 at 16:27