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)

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

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.


Goncharov, S., Rauch, C., & Schröder, L. (2018). A Metalanguage for Guarded Iteration. In Bernd Fischer Tarmo Uustalu (Eds.), Theoretical Aspects of Computing - ICTAC 2018 (LNCS 11187) (pp. 191--210). Stellenbosch, South Africa: Springer International Publishing.
Goncharov, S., & Neves, R. (2018). A Semantics for Hybrid Iteration. In Proceedings of the 29th International Conference on Concurrency Theory, CONCUR 2018. Beijing, China.
Goncharov, S., & Schröder, L. (2018). Guarded Traced Categories. In Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 (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 2019-16-04 at 14:20