Thomas Streicher (* 11. Februar 1958 in Linz, Österreich; † 2. Januar 2025 in Darmstadt)[1] war ein österreichischer Mathematiker und Professor an der Technischen Universität Darmstadt. Er war bekannt für seine Arbeiten in den Bereichen Typentheorie, kategoriale Logik, Domänentheorie[2] und den logischen Grundlagen des Funktionalen Programmierens.[1]
Thomas Streicher wurde am 11. Februar 1958 in Linz in Österreich geboren. Er wurde 1988 an der Universität Passau unter der Betreuung von Manfred Broy mit der Dissertation Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions promoviert.[3]
Nach seiner Promotion begann Streicher eine akademische Karriere, die ihn schließlich 1995 als Professor an die Technische Universität Darmstadt führte. Dort forschte und lehrte er bis zu seiner Emeritierung im April 2024. Am 2. Januar 2025 starb er.
Thomas Streicher hatte breitgefächerte Interessen, in und außerhalb der Mathematik. Internationale Beachtung erlangte er insbesondere durch seine Beiträge zur Martin-Löf-Typentheorie,[4] kategorialen Logik und zur Domänentheorie und den logischen Grundlagen des funktionalen Programmierens. Er war einer der Begründer der Homotopy Type Theory,[5] die ab den 2000er Jahren weltweit Beachtung fand.[1][6]
Seine bekanntesten Beiträge sind:
Gemeinsam mit Martin Hofmann entwickelte er ein Modell für die intensionale Martin-Löf-Typentheorie,[4] bei dem Identitätstypen als Gruppoide interpretiert werden. Dies war das erste Modell mit nicht-trivialen Identitätstypen (Identitäten, die nicht auf Mengen basieren).[7] Dieses Modell beeinflusste später die Entwicklung der Homotopy Type Theory[5] und die Univalent Foundations der Mathematik.[6]
Seine Dissertation und späteren Arbeiten behandelten die Korrektheit und Vollständigkeit von Semantischen Modellen der Typentheorie.
Streicher beschäftigte sich intensiv mit den Grundlagen der funktionalen Programmierung, insbesondere mit der Anwendung der Domänentheorie auf die Semantik von Programmiersprachen.
Zu seinen wichtigsten Arbeiten zählen:
Die Arbeiten von Thomas Streicher haben die theoretischen Grundlagen der Typentheorie und ihre Anwendung in der Informatik maßgeblich geprägt. Insbesondere seine Beiträge zur Interpretation der Identitätstypen gelten als Meilenstein in der Entwicklung der Homotopy Type Theory.[7]
| Personendaten | |
|---|---|
| NAME | Streicher, Thomas |
| KURZBESCHREIBUNG | österreichischer Mathematiker |
| GEBURTSDATUM | 11. Februar 1958 |
| GEBURTSORT | Linz, Österreich |
| STERBEDATUM | 2. Januar 2025 |
| STERBEORT | Darmstadt |