Lineare Typen und Session Typen für Funktionale Programme

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

Verhaltenstypen beschreiben Zustandsänderungen von Objekten zur Übersetzungszeit in Form von Protokollen, d.h. erlaubte Abfolgen von Operationen auf den Objekten. Durch die Verwendung solcher Typen kann ein Compiler die korrekte Verwendung der Objekte analysieren und garantieren, dass das Protokoll zur Laufzeit eingehalten wird. Es gibt viele Arten von Verhaltenstypen, die unterschiedliche Garantien liefern. Beispiele hierfür sind allgemeine Typestate-Protokolle sowie Sessiontypen (für typkorrekte und protokollsichere Kommunikation). Ein Problem ergibt sich hierbei durch Aliasing, d.h., wenn es mehrere Referenzen zum selben Objekt gibt, weil dies die Überprüfung der Protokolle erschwert. Borrowing ist eine Instanz dieses Problems, bei der Aliase explizit erstellt werden müssen; ein aktuelles Konzept, das durch Rust Popularität erhielt. Wir wollen eine neue Grundlage für Verhaltenstypen in der Form von Typestate mit Borrowing erforschen. Unser neuer Ansatz basiert auf Zustandsübergängen anstelle von Zuständen. Dies steht in Kontrast zu den bisherigen Arbeiten, die den Zustandsübergang eines Objekts (oder Borrow) in einer Funktion durch ein Paar von Eingabe- und Ausgabezustand spezifizieren. Stattdessen verwendet unser Ansatz eine Abstraktion von Zustandsübergängen, die durch ein geordnetes partielles Monoid gegeben ist. Darüber hinaus wollen wir Borrowing nicht mit ad-hoc Methoden behandeln, sondern wir werden die Theorie der geordneten Typen (eine Verfeinerung von linearen Typen) als logische Grundlage verwenden.

• DFG-Verfahren: Sachbeihilfen