Matija Pretnar: Dokazovalni pomočnik Abella
Date of publication: 7. 11. 2016
Mathematics and theoretical computing seminar
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.
