Andrej Bauer: Implementacija teorije tipov s pravilom refleksije

Datum objave: 30. 3. 2015
Seminar za temelje matematike in teoretično računalništvo
Torek, 31. marec 2015, od 12h do 14h, Plemljev seminar, Jadranska 19

Povzetek: Teorija tipov s pravilom refleksije ima precej slabše lastnosti kot standardna Martin-Löfova teorija tipov, kljub temu pa je zanimiva za formalizacijo nekaterih zvrsti matematike. Pojavi se vprašanje, kako načrtovati dokazovalni pomočnik za delo s tako teorijo tipov. Na seminarju bom predstavil trenutno zasnovo pomočnika, ki ga razvijamo v sklopu projekta Effmath.

Predavanje bo v angleščini. Vabljeni!