Lezioni TEORIA dei TIPI - 2016/17

Seminari introduttivi al proof-assistant Coq Relatore: Enrico Tassi Date: 31 maggio e 1-7-8 giugno ore 13.30-15.30 in laboratorio TA note 2017 aggiornate al 25/5 Scrivetemi se trovate errori! Testi di riferimento: Programming in Martin-Loef's Type Theory P. Martin-Loef- Intuitionistic type theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980, Bibliopolis 1984. Per approfondimento: "La teoria dei tipi" To appear in "Direzioni della ricerca logica in Italia 2", ETS, eds. H.Hosni, G. Lolli, C. Toffalori (in Italian) note 2016 Scrivetemi se trovate errori!