PROVA orale su esercizi assegnati precedentemente
dal docente (svolti su carta o con utilizzo del proof-assistant)
su richiesta: prova parziale orale a meta' corso dopo il 15 aprile in giorno concordato con il docente
Ricevimento :
disponibile via Zoom
(previo appuntamento via email con identificazione nome e cognome studente).
Siete pregati di utilizzare esclusivamente l'email accademica.
AVVISI
inizio del corso: mercoledi' 3/3 ore 16.30
modalita' erogazione corso: duale in presenza e telematica sincrona/asincrona tramite video pubblicati
nella pagina moodle del corso di teoria dei tipi
mercoledi' dalle 16.30 alle 18
giovedi' dalle 14.30 alle 16
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"
in "Direzioni della ricerca logica in Italia 2", ETS, eds. H.Hosni, G. Lolli, C. Toffalori (in Italian)
P. Wadler's textbook ``Programming Language Foundations in Agda" as a literate script in Agda freely available with a paper presentation here
(per informatici)