A High Level Language for Programming and Specifying Multi-Effect Algorithms

Third party funded individual grant

Project Details

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

Project members:
PD Dr.-Ing. Sergey Goncharov

Contributing FAU Organisations:
Lehrstuhl für Informatik 8 (Theoretische Informatik)

Funding source: DFG-Einzelförderung / Sachbeihilfe (EIN-SBH)
Acronym: HighMoon
Start date: 01/09/2013

Abstract (technical / expert description):

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.

Last updated on 2018-06-11 at 17:45