Bei der Implementierung funktionaler Sprachen ist heutzutage eine automatische Speicherverwaltung in Form eines Tracing Garbage Collectors Standard und hat frühere Implementierungen mittels Referenzzählung weitestgehend abgelöst. Im Spezialfall von
pur funktionalen Sprachen kann optimierte Referenzzählung aber auch heute noch kompetitive Laufzeiten ergeben, wie unserem
Paper gezeigt. Ein Bestandteil davon ist eine Intermediate Representation, die explizite Instruktionen zur Referenzzählung enthält, sowie ein Compiler in diese. Die Arbeitsweise des Compilers wurde in einem
vorläufigen Appendix relativ zu einem Typsystem als korrekt bewiesen; jedoch ist dabei eine technische Komplexität erreicht, bei der Papierbeweise nicht mehr unbedingt vertrauenswürdig sind. In dieser Arbeit sollen daher der Beweis und dafür benötigte Konstruktionen wie das Typsystem im Theorembeweiser
Lean formalisiert werden, um eine vertrauenswürdigere Korrektheitsaussage zu erhalten.
Aufgabe:
Formalisierung des Compilerbeweises und benötigter Abhängigkeiten aus obigem Appendix in Lean
Voraussetzungen
- Grundkenntnisse in formalen Systemen
Schlüsselworte
Lean, Programmverifikation, Compiler
Veröffentlichungen
Betreuer
Studenten
