Témavezetés adatlap
Mészáros Botond
hallgató
témavezetés címe
Setoid típuselmélet
intézmény
doktori iskola
témavezető
témavezetés módja
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.
képzés kezdete
2025-09-01
abszolutórium megszerzésének várható ideje
2029-09-01
státusz
folyamatban lévő
témakiírás
témakiírás címe