Lean ist eine an unserem Lehrstuhl mitentwickelte pur funktionale Programmiersprache als auch ein Theorembeweiser. Obwohl in einer puren Funktion keine beobachtbaren Nebeneffekte erlaubt sind, kann die Lean-Laufzeitumgebung durch Verwendung von Referenzzählung Werte "destruktiv" verändern statt neue zu allokieren, solange der bisherige Wert nur einmal referenziert war (
Veröffentlichung). Dieser Kniff erlaubt es insbesondere, Arrays wie in imperativen Sprachen zu verwenden.
Da diese Optimierung aber dynamisch zur Laufzeit angewendet wird, obliegt es bisher dem Programmierer sicherzustellen, dass entsprechende Werte an performancekritischen Stellen tatsächlich nur einmal referenziert, ab Erstellung also linear benutzt wurden. Um Entwicklung und Pflege solches Codes zu vereinfachen, soll in dieser Arbeit eine statische Analyse, also zum Beispiel ein Typsystem, entwickelt werden, das diese Eigenschaften stattdessen zur Kompilierzeit überprüft. Als Erweiterung können diese Garantien dann auch benutzt werden, um den erzeugten Code durch Entfernen der entsprechenden Laufzeitchecks zu optimieren.
Schlüsselworte
Lean, Typsysteme, Referenzzählung
Veröffentlichungen
Betreuer
Studenten
