témavezető: Kozsik Tamás
helyszín (magyar oldal): ELTE Informatikai Kar helyszín rövidítés: ELTE
A kutatási téma leírása:
A típuselmélet a konstruktív matematika megalapozására használható logikai kalkulus. Implementációi (pl. Agda, Coq, NuPRL, Idris) programozási nyelvként és tételbizonyító rendszerként is használhatók.
A nyers típuselméleti kifejezések a gyakorlatban nehezen olvashatók. Például a függvénykompozíció teljes típusa "(A B C : Type)
-> (B -> C) -> (A -> B) -> (A -> C)", de az első három paraméter (A, B
és C) kikövetkeztethető a további paraméterekből, ezért informálisan nem írjuk ki őket. Formálisan metaváltozóknak nevezzük ezeket, és a típusellenőrző egységesítés fázisa következteti ki értéküket. A kutatási téma egy ezen metaváltozókra vonatkozó egységes kalkulus kidolgozása, melyben a típusellenőrzés és a metaváltozók kikövetkeztetése egyszerre történik, és egy hatékony implementáció létrehozása.
A téma pontos egyeztetése a hallgatóval együtt történik majd.