30214 - FONDAMENTI LOGICI DELL'INFORMATICA

Conoscenze e abilità da conseguire

Al termine del corso, lo studente conosce le basi logico formali dell'informatica, in particolare, il lamb da calcolo e la sua teoria, corrispondenza tra programmi e dimostrazioni, il lamb da calcolo tipato semplice, i sistemi T ed F. È in grado di descrivere semplici funzioni numeriche in lamb da calcolo e di derivarne i tipi.

Contenuti

Il corso presenta la corrispondenza tra programmi e dimostrazioni (rispettivamente, tipi e enunciati), nota anche come corrispondenza di Curry-Howard.  
La prima parte del corso è un'introduzione al lambda calcolo senza tipi: sintassi, riduzione, completezza algoritimica, confluenza, separabilità (cenni).
La seconda parte del corso studia calcoli tipizzati di potere espressivo crescente, con particolare interesse alle logiche alle quali corrispondono: lambda calcolo tipizzato semplice e logica intuizionista, sistema T, sistema F, tipi dipendenti, calcolo delle costruzioni (cenni). Viene analizzato il potere espressivo di questi calcoli, e si presentano alcune tecniche per la dimostrazione di normalizzazione.

Testi/Bibliografia

H.Barendregt. Lambda Calculi with Types. Handbook of Logic in Computer Science, Volumes 1. Clarendon, 1992 Disponibile online a  http://www.cs.unibo.it/~martini/FLI/barendregt.pdf . 
J.-Y. Girard. Proof and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University press. 1989.  Esaurito. Disponibile on-line a  http://www.paultaylor.eu/stable/prot.pdf .

Metodi didattici

Lezioni frontali

Modalità di verifica e valutazione dell'apprendimento

Esame orale

Strumenti a supporto della didattica

Lezioni alla lavagna.

Orario di ricevimento

Consulta il sito web di Simone Martini

Consulta il sito web di Claudio Sacerdoti Coen