Matija Pretnar: Dokazovalni pomočnik Abella
Datum objave: 7. 11. 2016
Seminar za temelje matematike in teoretično računalništvo
Torek, 8. 11. 2016, od 12h do 14h, Plemljev seminar, Jadranska 19
Povzetek: Ogledali si bomo dokazovalni pomočnik Abella ter z njim dokazali varnost in enoličnost tipov za λ-račun s preprostimi tipi.
Abstract: We will take a look at the Abella proof assistant and use it to prove safety and uniqueness of types for simply typed λ-calculus.
