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
