per il corso di Laurea Specialistica
in Informatica
e il corso di Laurea in Matematica
a.a. 2003/2004
docente Silvio Valentini
Periodo
Il corso si svolge nel primo trimestre, a partire dal 13 ottobre
2003 fino al 9 dicembre 2003.
Prerequisiti
Questo corso si rivolge ad uno studente che abbia preferibilmente
seguito il primo modulo del corso di Istituzioni di Logica Matematica e che intenda
approfondire lo studio dei legami tra la Logica Matematica e gli aspetti più
teorici dell'Informatica. Può essere conveniente, ma non è assolutamente
necessario, aver seguito anche il modulo B del corso di Istituzioni di Logica
Matematica.
Scopo del corso
Visto il profondo legame esistente a livello teorico tra i linguaggi
funzionali tipati e i sistemi logici intuizionisti, lo scopo di questo corso è
quello di fornire una introduzione teorica ai linguaggi di programmazione funzionali
tipati e non tipati.
Programma del corso
Dopo aver analizzato il lambda calcolo tipato semplice (4 ore),
ed i suoi legami con il frammento implicativo del calcolo proposizionale intuizionista
(2 ore), si intendono studiare lambda calcoli con tipi di carattere più
generale. Si introdurrano dapprima il calcolo con tipi dipendenti, che rappresenta
il contenuto computazionale della logica del primo ordine (8 ore), per continuare
poi con calcoli con tipi di secondo ordine, potenti quanto l'aritmetica di Heyting
al secondo ordine (10 ore), e finire quindi con calcoli estremamente potenti che
considerano entrambi i sistemi di tipi (8 ore) ed eventualmente anche i tipi induttivamente
generati (6 ore). Per tutti tali lambda calcoli si intendono dimostrare i principali
teoremi matematici, vale a dire il teorema di normalizzazione e di confluenza,
e fornire esempi di applicazione in informatica teorica.
Testi di riferimento
J.Y.Girard, Y.Lafont, P.Taylor, Proofs and Types
H.Barendreght, The Lambda Calculus, its Syntax and Semantics