Logica 2 - Logica matematica (mod. B)

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

H.Barendreght, Lambda Calculi with Types

[Back]