Auszeichnung für herausragende Dissertation

Dr. Joachim Breitner wurde vom KIT-Präsidium für seine an der KIT-Fakultät für Informatik abgelegte Disseration mit dem Titel „Lazy Evaluation: From natural semantics to a machine-checked compiler transformation” mit dem KIT-Doktorandenpreis ausgezeichnet. Der mit je 1.500€ dotierte KIT-Doktorandenpreis gilt als Auszeichnung herausragender Promovierter und soll den hohen Stellenwert des wissenschaftlichen Nachwuchses und der vielfältigen Forschungsmöglichkeiten am KIT unterstreichen. Ausschlaggebend für die Nominierung sind unter anderem die internationale Sichtbarkeit, Mobilität und Vernetzung, Selbständigkeit und Eigeninitiative, Lehr- und Betreuungskompetenz, der Erwerb überfachlicher Kompetenzen, Engagement und Promotionsdauer der Bewerber. Aktuell arbeitet Joachim Breitner als Postdoktorand an einem US-nationalen Forschungsprojekt zur Software-Sicherheit an der University of Pennsylvania. Aus der Ferne bedankt sich der KIT-Doktorandenpreisträger: „Die Auszeichnung hat mich sehr gefreut und mir geschmeichelt. Es ist eine sehr schöne Art und Weise, auch in der Ferne ‚meiner‘ Universität verbunden zu bleiben.“

Joachim Breitner absolvierte ein Doppelstudium der Mathematik und Informatik am Karlsruher Institut für Technologie und schloss beide Studiengänge mit dem jahrgangsbesten Diplom ab. Als ein Stipendiat der Deutschen Telekom Stiftung war Herr Breitner seit 2012 Doktorand am Lehrstuhl Programmierparadigmen von Prof. Gregor Snelting wo er letztes Jahr seine Promotion mit summa cum laude abschloss. 

In seiner Dissertation geht Dr. Joachim Breitner der Frage nach, wie sich mit Hilfe formaler Semantiken von Programmiersprachen beweisen lässt, dass eine Programmtransformation, wie sie der Compiler vornimmt, tatsächlich auch eine Optimierung ist. Im ersten Teil seiner Arbeit gelang es Herrn Breitner eine seit Jahrzehnten offene Lücke in einem Beweis von Launchbury zur formalen Semantik funktionaler Sprachen zu schließen. Hierzu formalisierte er Launchburys Semantik für Sprachen mit Bedarfsauswertung im generischen Beweisassistenten „Isabelle“ um seine Beweise maschinell zu prüfen. Im Anschluss arbeitete Joachim Breitner während eines dreimonatigen Aufenthalts in Cambridge am Microsoft Research Center zusammen mit Simon Peyton-Jones, einem der Designer der Programmiersprache „Haskell“. Eine Optimierung der funktionalen Sprache „Haskell“, die „Call Arity“, wurde von Joachim Breitner vollständig neu entwickelt und programmiert und ist nun Teil des „Glasgow Haskell Compilers“ (GHC). Die Verifikation und Validierung der „Call Arity“ bilden den zweiten Teil der Dissertation.

Neben seiner international anerkannten Forschung engagierte sich Herr Breitner sowohl in der Lehre als auch im sozialen Bereich. So wurde er für seinen Erfolg als Übungsleiter mit mehreren Fakultätspreisen ausgezeichnet, trug zur Durchführung der „Gulaschprogrammiernacht“ bei und organisierte mehrere Veranstaltungen für Schüler.