Home » Archivo » Archvio 2009 » Fondamenti logici dei linguaggi funzionali - 2009/2010

Laurea Magistrale

Salta il menu di secondo livello

Fondamenti logici dei linguaggi funzionali - 6 CFU - A.A. 2009/2010

Insegnante

Prof. Silvio Valentini

Periodo

I anno - 3 trimestre | 06/04/2010 - 11/06/2010

Curriculum:

Ore: 40 Frontali, 0 Laboratorio, 8 Esercizi

Torna su ▲

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.

Prerequisiti: Logica Matematica

Propedeuticità:

Ausili Didattici: J.Y.Girard, Y.Lafont, P.Taylor, Proofs and Types, Cambridge University Press H.Barendreght, The Lambda Calculus, its Syntax and Semantics, North-Holland H.Barendreght, Lambda Calculi with Types (Handbook of Logic in Computer Science), Oxford University Press.

Testi di Riferimento: Appunti del docente.

Torna su ▲