In seiner PhD-Thesis hat Olin Shivers ein Verfahren präsentiert, um Kontrollflussgraphen für funktionale Sprachen zu erstellen. Damit sind Standardoptimierungen aus dem Compilerbau auch für funktionale Sprachen möglich.
Aufgabe:
In dieser Studienarbeit soll der Ansatz von Shivers für eine einfache funktionale Sprache in Isabelle/HOL formalisiert werden. Ein Beweis soll garanitieren, dass die CFA-Abstraktion auch wirklich konkrete Programme abstrahiert.
Falls möglich, soll auch geprüft werden, ob es der Ansatz von Shivers ermöglicht, das modulare Slicing-Framework, das hier am Lehrstuhl entwickelt wurde, mit funktionalen Sprachen zu instanitiieren.
Veröffentlichungen
Betreuer
Studenten
