Andrej Bauer: Andromedanska teorija tipov

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!