Teoria costruttiva dei tipi e teoria delle categorie

Responsabile didattico: Marino Miculan

Durata: 28 ore

Periodo didattico: annuale

Programma

SETTORE SCIENTIFICO DISCIPLINARE: INF/01

28h - prof. Marino Miculan con interventi di Pietro Corvaja e Furio Honsell

 

"Teoria Costruttiva dei Tipi e Teoria delle Categorie"

Il corso si rivolge a studenti di matematica, informatica e filosofia. È possibile definire percorsi personalizzati sulla base di specifici interessi.

In questa serie di incontri vengono introdotte le nozioni fondamentali di Teoria Costruttiva dei Tipi e di Teoria delle categorie, che negli ultimi decenni hanno permesso di stabilire un nesso concettuale molto forte tra settori apparentemente lontani della matematica, filosofia, logica, linguistica, e informatica, quali: i fondamenti della matematica, la teoria dei linguaggi di programmazione, la certificazione logica dei programmi, la topologia algebrica.

Il corso sarà articolato in tre parti: in una prima parte, verranno forniti agli studenti le basi del lambda calcolo e? della teoria costruttiva dei tipi, nella seconda parte verrà introdotta la teoria delle categorie, ed infine nella terza parte verranno mostrate le connessioni tra teoria dei tipi, lambda calcolo e categorie cartesiane chiuse, collocandole nel contesto della logica categoriale. Infine verrà presentato il concetto di monade, alla base di linguaggi moderni come Haskell.

 

Programma di massima:

1) 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

 

2) Introduzione alla teoria delle categorie

- Definizione di categorie, funtori e trasformazioni naturali

- Categorie di funtori, Lemma di Yoneda

- Limiti e colimiti

- Aggiunzioni

 

3) Applicazioni alla teoria dei tipi

- Strutture (monoidali) ?cartesiane chiuse

- Logica categoriale: lambda calcolo e categorie cartesiane chiuse

- Monadi e teorie di Lawvere

 


Elenco corsi 2020/2021