Teoria costruttiva dei tipi e teoria delle categorie
a.a. 2020/21
Responsabile didattico: Marino Miculan
Docenti: Marino Miculan, Pietro Corvaja, Furio Honsell
Durata: 28 ore
Programma: Introduzione alla teoria dei tipi: tipi e invarianti; lambda calcolo e programmazione funzionale (ML, CAML, …); Teoria Costruttivi dei Tipi di Martin-Löf; corrispondenza formule-come-tipi e dimostrazioni-come-algoritmi; Certificazione formale del software: Logical Frameworks e Coq; Homotopy Type Theory e connessioni con la topologia algebrica. Introduzione alla teoria delle categorie: definizione di categorie, funtori e trasformazioni naturali; categorie di funtori, Lemma di Yoneda; limiti e colimiti; Aggiunzioni. Applicazioni alla teoria dei tipi: Strutture (monoidali) cartesiane chiuse; Logica categoriale: lambda calcolo e categorie cartesiane chiuse; Monadi e teorie di Lawvere.