Lineare Typen und Session Typen für Funktionale Programme

• Antragsteller: Professor Dr. Peter Thiemann
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2018 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 395068988

Microservices haben wesentlichen Anteil am Stand der Technik bei der Konstruktion von Infrastrukturen für verteilte Anwendungen. Die Infrastruktur und auch die Anwendung bestehen aus Komponenten, die Microservices implementieren und dafür gemäß eines global orchestrierten Protokolls miteinander kommunizieren. Ein Session-Typ ist eine leichtgewichtige Spezifikation für ein orchestriertes und strukturiertes Protokoll, die während der Übersetzung vom Compiler/Typchecker überprüft wird. Ein Session-Typ liefert eine Reihe von wichtigen Garantieen für sämtliche Kommunikationen einer Komponente: Typsicherheit, Sitzungstreue und Freiheit von Deadlocks. Eine Programmiersprache, deren Typsystem Session-Typen unterstützt, wäre ein gewaltiger Fortschritt für die Entwickler von Komponenten, denn sie vermeidet durch die Garantieen eine ganze Klasse von Fehlern und verringert dadurch den Aufwand für die aufwendige Fehlersuche in verteilten Anwendungen.Keine der heutigen Programmiersprachen für Komponenten unterstützt Session-Typen. Ein Grund dafür liegt darin, dass schon Linearität, ein Grundbaustein für Session-Typen, nicht unterstützt wird. Weitere fortgeschrittene Typsystemkonzepte (z.B. Typfunktionen) sind in manchen Sprachen vorhanden, aber nicht in der notwendigen Ausprägung. Linearität und Typfunktionen zusammen können sicherstellen, dass alle Teilnehmer an einem Protokoll die Reihenfolge, die Richtung und den Typ der Nachrichten beachten und dass kein Teilnehmer vorzeitig aus dem Protokoll aussteigt.Das Ziel dieses Projekts ist die Erforschung der theoretischen Grundlagen zur Erweiterung einer Programmiersprache um Linearität und Session-Typen und ihre praktische Umsetzung. Das resultierende Framework soll durch eine Implementierung in einer industriell angewendeten Sprache, die zur Programmierung von kommunizierenden Komponenten geeignet ist, praktisch validiert werden. Im Projekt soll zusätzliche Infrastruktur entworfen und implementiert werden, mit deren Hilfe die High-Level Session-Typen auf existierende Infrastrukturen und Protokollsoftware abgebildet werden können. Diese Infrastruktur ist wichtig zur Integration von Session-getypten Komponenten in eine Microservice Architektur.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Großbritannien, Japan
• Kooperationspartnerinnen / Kooperationspartner: Professor Dr. Jacques Garrigue; Professor Dr. Keigo Imai; Professorin Nobuko Yoshida; Professor Dr. Shoji Yuen