Témavezetés adatlap
Bense Viktor
hallgató
témavezetés címe
Setoid típuselmélet
intézmény
doktori iskola
témavezető
témavezetés módja
egyéni
fokozat típusa
PhD
témavezetés leírása
A függő típuselmélet egy olyan programozási nyelv, melyben egy program típusa matematikai állításnak, az adott típusú program pedig az állítás bizonyításának tekinthető. A Martin-Löf típuselmélet
egyenlőség típusával lehet kifejezni két program egyenlőségét. Az
egyenlőség egy induktívan megadott típus, melynek hiányossága, hogy az ugyanahhoz a bemenethez ugyanazt a kimenetet rendelő programok illetve a logikailag ekvivalens állítások nem egyenlőek. Ezeket a tulajdonságokat axiómaként hozzávehetjük a típuselmélethez, de akkor az ezeket az axiómákat tartalmazó programok végrehajtása elakad. Kutatásunk célja a Martin-Löf típuselmélet kiegészítése a fenti tulajdonságokkal úgy, hogy a programok végrehajthatók maradjanak. Ehhez a típuselmélet setoid modellje adja az inspirációt, melyben egy típust egy halmazzal és egy azon értelmezett ekvivalencia-relációval értelmezünk. Az így kapott setoid típuselmélet a homotópia-típuselmélet alsó szintjének egy implementációja.
A téma pontos egyeztetése a hallgatóval együtt történik majd.
képzés kezdete
2023-09-01
abszolutórium megszerzésének várható ideje
2027-08-31
státusz
folyamatban lévő
témakiírás
témakiírás címe
további témavezetések