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.
előírt nyelvtudás: angol felvehető hallgatók száma: 1
Jelentkezési határidő: 2024-05-31
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Bejelentkezés
