A High Level Language for Monad-based Processes

• Applicants: Privatdozent Dr.-Ing. Sergey Goncharov; Professor Dr. Lutz Schröder
• Subject Area: Theoretical Computer Science
• Term: from 2012 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 215418801

• Final Report Year: 2022

Final Report Abstract

Während ideale mathematische Funktionen allein durch ihr Ein- und Ausgabeverhalten bestimmt sind, beinhaltet das Verhalten von Programmen in fast allen Programmierparadigmen Seiteneffekte verschiedenster Art wie etwa Zustandsbehaftetheit, Kommunikation, Ein- und Ausgabe, Zufälligkeit oder Nichtdeterminismus. Solche Seiteneffekte erschweren die Analyse und Verifikation von Programmen regelmäßig erheblich, insbesondere durch ihre Interaktion mit Nebenläufigkeit und Kontrollstrukturen wie Schleifen und Iteration. Als vereinheitlichender Rahmen für die Behandlung von verschiedenen Seiteneffekten hat sich die algebraische Modellierung mittels Monaden etabliert, die zum Beispiel in den funktionalen Programmiersprachen Haskell und F# als unterliegender Formalismus für imperative Aspekte dient. Gegenstand von HighMoon war die Entwicklung monadenbasierter generischer Methoden in diesem Sinne für die semantische und logische Behandlung von Seiteneffekten in Programmiersprachen. Besonderes Augenmerk lag dabei auf einem kanonischen Schleifenkonstrukt, der Iteration. Iteration wird hierbei axiomatisiert als eine der unterliegenden Monade innewohnende Operation. Sie kann abhängig von der Monade sehr verschiedene Ausprägungen haben; neben dem bekannten Verhalten rein imperativer Schleifenkonstrukte kann dies insbesondere auch die Form iterierter Prozesse, in denen zwischen den einzelnen Iterationen einer Schleife die Kontrolle an die Umgebung abgegeben wird, annehmen. Eine zentrale Rolle bei der Analyse von Iteration spielt hierbei die Unterscheidung zwischen bewachter und unbewachter Iteration; die erstere Form ist auf Schleifenkörper beschränkt, die in jedem Durchlauf in geeignetem Sinn einen Fortschritt der Berechnung garantieren, während die zweitere Form unbeschränkt anwendbar ist. In HighMoon haben wir unter anderem eine vereinheitlichte Axiomatik entwickelt, die durch Parametrisierung über Bewachtheitsbegriffe beide Formen von Iteration einheitlich behandelt, und im Rahmen dieser Theorie gezeigt, dass unbewachte Iteration stets durch Kollaps aus bewachten Iterationsoperationen entsteht. Wir haben diese Theorie im Kontext hybrider Berechnungen, die kontinuierliches und diskretes Verhalten verbinden, angewendet und insbesondere eine Monade für hybride Berechnungen mit Iteration identifiziert, auf deren Grundlage wir eine hybride Kernprogrammiersprache entwickelt und in einem Theorembeweiser formalisiert haben. In weiteren Projektresultaten haben wir eine generische Floyd-Hoare-Logik zur Verifikation von seiteneffektbehafteten Programmen mit Ausnahmebehandlung bereitgestellt sowie einen generischen Automatenlernalgorithmus entwickelt, der nicht nur zahlreiche bekannte Lernalgorithmen, etwa für ω - Automaten oder nominale Automaten, auf ein gemeinsames Fundament stellt, sondern auch zu neuen Lernalgorithmen z.B. für Kostenfunktionen instanziiert.

Publications

• Generic Hoare logic for orderenriched effects with exceptions. In IFIP WG 1.3 International Workshop on Recent Trends in Algebraic Development Techniques, WADT 2016, vol. 10644 of LNCS, pp. 208–222. Springer, 2016. (Section II.3.2)
  Christoph Rauch, Sergey Goncharov & Lutz Schröder
  
• A metalanguage for guarded iteration. In Theoretical Aspects of Computing, ICTAC 2018, vol. 11187 of LNCS, pp. 191– 210. Springer, 2018. Best Paper Award. (Section II.3.1)
  Sergey Goncharov, Christoph Rauch & Lutz Schröder
  
• A semantics for hybrid iteration. In Concurrency Theory, CONCUR 2018, vol. 118 of LIPIcs, pp. 22:1–22:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. (Section II.3.4)
  Sergey Goncharov, Julian Jakob & Renato Neves
  
• Guarded traced categories. In Foundations of Software Science and Computation Structures, FoSSaCS 2018, vol. 10803 of LNCS, pp. 313–330. Springer, 2018. EATCS Best Theory Paper Award. (Section II.3.1)
  Sergey Goncharov & Lutz Schröder
  
• Unguarded Recursion on Coinductive Resumptions. Logical Methods in Computer Science, Volume 14, Issue 3.
  Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph & Jakob, Julian
  
• Coinductive resumption monads: Guarded iterative and guarded Elgot. In Algebra and Coalgebra in Computer Science, CALCO 2019, vol. 139 of LIPIcs, pp. 13:1–13:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. (Section II.3.1)
  Paul Blain Levy & Sergey Goncharov
  
• Guarded and Unguarded Iteration for Generalized Processes. Logical Methods in Computer Science, Volume 15, Issue 3.
  Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph & Piróg, Maciej
  
• Automata Learning. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 900-914. ACM.
  Urbat, Henning & Schröder, Lutz
  
• Local local reasoning: A BI-hyperdoctrine for full ground store. In Foundations of Software Science and Computation Structures, FOSSACS 2020, vol. 12077 of LNCS, pp. 542–561. Springer, 2020. (Section II.3.3)
  Miriam Polzer & Sergey Goncharov
  
• Towards constructive hybrid semantics. In Formal Structures for Computation and Deduction, FSCD 2020, vol. 167 of LIPIcs, pp. 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. (Section II.3.4)
  Tim Lukas Diezel & Sergey Goncharov