Andrej Bauer: Implementacija teorije tipov s pravilom refleksije

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!