Ungarn forschen zu HOTT

Unter 928 eingereichten Bewerbungen in der Forschungskategorie  Naturwissenschaften und Technik wurden 131 ausgewählt. Der ERC (Europäischer Forschungsrat) prämiert die vielversprechendste Forschung im Rahmenprogramm Horizon Europe, von der explorativen Forschung bis zur ersten Phase der Nutzung. Mit der Consolidator Grant-Förderung werden Arbeiten gewürdigt, die bereits über eine Forschungsgruppe und herausragende Ergebnisse verfügen und einen wissenschaftlichen Durchbruch versprechen.

Kaposi und sein Team können mit ihrer Forschung zur Higher Observational Type Theory (HOTT) den Einsatz computergestützter Beweissysteme revolutionieren. Die Typentheorie bietet eine Lösung für die Beweis- und Korrektheitsprobleme von Mathematikern und Informatikern und gibt ihnen ein formales Sprachwerkzeug an die Hand, mit dem sie gleichzeitig Programme und mathematische Beweise schreiben können. Ziel des HOTT-Projekts ist die Entwicklung einer neuen Version der Homotopie-Typentheorie, bei der die höherdimensionale Geometrie nicht von Hand eingebaut, sondern emergent wird. Langfristig wird die neue Typentheorie zur Entwicklung der Computerverifizierung mathematischer Beweise und der Korrektheit von Software beitragen, indem sie abstrakte, wieder verwendbare Beweise ermöglicht.

Ambrus Kaposi ist außerordentlicher Professor an der Fakultät für Programmiersprachen und Übersetzungsprogramme der ELTE in Budapest. Er promovierte in klinischer Medizin und Informatik. Seine Forschungsgebiete sind Typentheorie, funktionale Programmierung, mathematische Logik und medizinische Statistik.