Projekt

Eine High-Level-Sprache für Monadenkombination

Ein etablierter Ansatz zur Überbrückung der durch Seiteneffekte bedingten konzeptuellen Lücke zwischen Programmen und mathematischen Funktionen ist die Verkapselung von Seiteneffekten mittels Monaden, d.h. polymorpher Typen von Berechnungen. Funktionen mit Seiteneffekten werden hierbei als reine Funktionen aufgefasst, die Berechnungen zurückgeben. Formale Grundlage dieses u.a. in den Programmiersprachen Haskell und F# verwendeten Prinzips ist Moggis Computational Metalanguage. Diese ist aber, ebenso wie auf ihr basierende generische Programmlogiken, gegenwärtig auf sequentielle Programmierung über relativ einfachen Speichermodellen beschränkt, während spezialisierte Programmlogiken wie auch die praktische monadische Programmierung mittlerweile komplexe Programmier- und Verifikationsparadigmen wie Nebenläufigkeit und Heap-Analyse unterstützen. Unser Ziel ist die Einbindung der nächsten Generation monadischer Programmierprinzipien und Programmlogiken in einem einheitlichen Rahmen, der High Level Monadic Metalanguage (HMML). Diese erweitert die über einem festen Effekt interpretierte Computational Metalanguage zu einer Metasprache über der Kategorie der Monaden und beinhaltet damit insbesondere explizite Konstrukte für Monadenmorphismen und kategorielle Konstruktionen auf Monaden. Für die HMML werden mechanische und, soweit möglich, automatische Beweiswerkzeuge entwickelt. Die HMML unterstützt insbesondere nebenläufige Prozesse mit generischen Seiteneffekten und generische Verifikationslogiken für Heap-Programme.

Projektleitung:
Prof. Dr. Lutz Schröder, PD Dr. Sergey Goncharov

Beteiligte:
Christoph Rauch, M. Sc.

Stichwörter:
Monaden; Seiteneffekte; Metasprache; abstrakte Programmierung

Laufzeit: 1.7.2013 - 30.6.2015

Förderer:
Deutsche Forschungsgemeinschaft

Kontakt:
Schröder, Lutz
Telefon 09131/85-64059, Fax 09131/85-64055, E-Mail: lutz.schroeder@fau.de

Publikationen

Goncharov, Sergey ; Schröder, Lutz: A coinductive calculus for asynchronous side-effecting processes. In: Information and Computation 231 (2013), S. 204–232

Goncharov, Sergey ; Schröder, Lutz: A Relatively Complete Generic Hoare Logic for Order-Enriched Effects. In: Kupferman, Orna (Hrsg.) : Proc. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013. Los Alamitos : IEEE Computer Society, 2013, S. 273-282. - ISBN 978-1-4799-0413-6
[doi>10.1109/LICS.2013.33]

Bowler, Nathan ; Goncharov, Sergey ; Levy, Paul Blain ; Schröder, Lutz: Exploring the Boundaries of Monad Tensorability on Set. In: Logical Methods in Computer Science 9 (2013), Nr. 3:22, S. 1-18
[doi>10.2168/LMCS-9(3:22)2013]

Goncharov, Sergey ; Pattinson, Dirk: Coalgebraic Weak Bisimulation from Recursive Equations over Monads. In: Esparza, Javier ; Fraigniaud, Pierre ; Husfeldt, Thore ; Koutsoupias, Elias (Hrsg.) : Proc. 41st International Colloquium on Automata, Languages, and Programming (ICALP 2014 Kopenhagen 08.-11.07.2014). Berlin/Heidelberg : Springer, 2014, S. 196-207. (Lecture Notes in Computer Science Bd. 8573)

Goncharov, Sergey ; Milius, Stefan ; Silva, Alexandra: Towards a Coalgebraic Chomsky Hierarchy. In: Diaz, Josep ; Lanese, Ivan ; Sangiorgi, Davide (Hrsg.) : Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS 2014 Rom 01.-03.09.2014). Bd. 8705. Heidelberg : Springer, 2014, S. 265-280. (Lecture Notes in Computer Science)
[doi>10.1007/978-3-662-44602-7_21]

Goncharov, Sergey ; Rauch, Christoph ; Schröder, Lutz: Unguarded Recursion on Coinductive Resumptions. In: Ghica, Dan (Hrsg.) : The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI) ((MFPS XXXI) Nijmegen (NL) 24.-26.06.2015). Bd. 319. 2015, S. 183-198. (Electronic Notes in Theoretical Computer Science)
[doi>10.1016/j.entcs.2015.12.012]