HOTT – Higher Observational Type Theory
Projektazonosító: 101170308
HORIZON.1.1 – Európai Kutatási Tanács (ERC)
ERC-2024-COG – ERC Consolidator Grant
Támogatás összege: 1 897 375,00 €
Kedvezményezett: Eötvös Loránd Tudományegyetem (ELTE)
Közreműködő szervezet: Programozási Nyelvek és Fordítóprogramok Tanszék, ELTE Informatikai Kar
ELTE PI/projektvezető: Dr. Kaposi Ambrus
Projekt kezdési dátuma: 2025. május 1.
Projekt tervezett befejezési dátuma: 2030. április 30.
Könnyen érthető nyelv a formális verifikációhoz
A matematika és a számítástechnika a formális verifikációra támaszkodik a következtetések helyességének és a kritikus fontosságú szoftverek biztonságának garantálása érdekében. A közelmúlt eredményei – például a négyszín-tétel formalizálása vagy a Google Chrome böngészőjében alkalmazott verifikált komponensek – jól szemléltetik a bizonyítássegítő rendszerek (proof assistants) erejét. Ezek az eszközök a típuselmélet nyelvén alapulnak. Bár az akadémiai szférában sikeresnek bizonyult, a homotópikus típuselmélet (Homotopy Type Theory – HoTT) bonyolult szintaxisa és fogalmi nehézségei miatt nem terjedt el széles körben. Ezt szem előtt tartva az ERC által finanszírozott HOTT projekt célja egy olyan új típuselmélet kidolgozása, amelyben a homotópikus tartalom természetes módon jelenik meg, ezáltal egyszerűsítve a folyamatot. Az egyenlőségi típusok számítási alapú definiálásával a projekt hozzáférhetőbbé teszi a formalizálást, felgyorsítva ezzel a fejlődést a matematika és a szoftververifikáció területén.
ERC HOTT – ERC-2024-COG – 101170308
Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or European Research Council Executive Agency (ERCEA). Neither the European Union nor the granting authority can be held responsible for them.
