Anwendung innovativer Programmierparadigmen

Programmieren mit Dependent Types

 Dependent Types sind eine Erweiterung traditioneller Typsysteme. Mit ihnen ist es möglich, nahezu beliebige Eigenschaften von Programmteilen zu spezifizieren. Die Überprüfung der Eigenschaften geschieht dabei im Rahmen der Typprüfung. Dadurch kann bereits der Compiler sicherstellen, dass z.B. Arraygrenzen eingehalten werden oder eine Sortierfunktion auch wirklich sortiert.

Bei diesem Thema geht es darum, Algorithmen und Datenstrukturen zu implementieren, die diese Möglichkeiten der Spezifikation und Verifikation nutzen. Dabei soll die Programmiersprache  Agda verwendet werden.

Integration von funktionaler und aspektorientierter Programmierung

 AspectML ist eine Programmiersprache, welche  funktionale und  aspektorientierte Programmierung miteinander vereinigt. In diesem Projekt soll eine Software in AspectML entwickelt werden. Außerdem soll analysiert werden, inwieweit sich die Features von AspectML mittels normaler funktionaler Programmierung simulieren lassen.

Kontakt: Petra Hofstedt Thomas König