Andrej Bauer: Andromedanska teorija tipov

Datum objave: 27. 10. 2014
Seminar za temelje matematike in teoretično računalništvo
Torek, 28. 10. 2014 od 12h do 14h, Plemljev seminar, Jadranska 19

Povztek: Obstoječi dokazovalni pomočniki, ki so zasnovani na teoriji odvisnih tipov, uporabljajo intenzionalno teorijo tipov in imajo popolno kontrolo nad preverjanjem enakosti termov. Na predavanju bom govoril o zasnovi dokazovalnega pomočnika, ki uporablja teorijo tipov s pravilom refleksije, kar omogoča uporabniku dosti večjo izrazno moč in poseganje v pojem enakosti. Tako lahko na primer dodaja nova računska pravila, kar vodi v razne tehnične komplikacije.

Predavanje je uvod v raziskovalno tematiko, s katero se bomo ukvarjali v sklopu projekta Effmath. 

Vabljeni!