Scheda insegnamento
-
Docente Simone Martini
-
Moduli Simone Martini (Modulo 1)
Claudio Sacerdoti Coen (Modulo 2)
-
Crediti formativi 6
-
SSD MAT/01
-
Modalità didattica Convenzionale - Lezioni in presenza (Modulo 1)
Convenzionale - Lezioni in presenza (Modulo 2)
-
Lingua di insegnamento Italiano
-
Campus di Bologna
-
Corso Laurea Magistrale in Informatica (cod. 8028)
Valido anche per Laurea Magistrale in Scienze filosofiche (cod. 8773)
Anno Accademico 2016/2017
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