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 24 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' 18/3 ore 14.30
modalita' erogazione corso: telematica asincrona tramite video pubblicati
nella pagina moodle del corso di teoria dei tipi
entro la data in cui si doveva tenere la lezione secondo orario ufficiale
esercizi sez. 3.1 note del corso ( aggiornati al 6/4!)
esercizi sez. 3.2 note del corso ( aggiornati al 6/4!)
man mano che un certo costruttore di tipi X viene trattato a lezione, si eseguano gli esercizi che seguono la descrizione delle regole
del tipo X nelle note del corso
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)
note 2020
aggiornate al 10/5 
