Presentazione

Organizzazione della Didattica

DM270
INFORMATICA ORD. 2014

Fondamenti logici dei linguaggi funzionali

6

Corsi comuni

 

Frontali Esercizi Laboratorio Studio Individuale
ORE: 40 8 0 102

Periodo

AnnoPeriodo
I anno1 semestre

Frequenza

Facoltativa

Erogazione

Convenzionale

Lingua

Italiano

Calendario Attività Didattiche

InizioFine
01/10/201424/01/2015

Tipologia

TipologiaAmbitoSSDCFU
affine/integrativo Nessun ambitoMAT/016


Responsabile Insegnamento

ResponsabileSSDStruttura
Prof. VALENTINI SILVIOMAT/01Dipartimento di Matematica

Altri Docenti

Non previsti

Attività di Supporto alla Didattica

Non previste

Bollettino

Conoscenze di base di logica matematica e del linguaggio insiemistico

Lo scopo di questo corso è quello di fornire una introduzione teorica ai linguaggi di programmazione funzionali tipati e non tipati.

Lezioni frontali in aula

Dopo aver richiamato la nozione di funzione calcolabile si introdurrà il lambda calcolo puro e si dimostrerà che esso è uno strumento universale di calcolo. Si analizzerà quindi il lambda calcolo tipato semplice ed i suoi legami con il frammento implicativo del calcolo proposizionale intuizionista. Si introdurrano poi il calcolo con tipi dipendenti, che rappresenta il contenuto computazionale della logica del primo ordine, per continuare con calcoli con tipi di secondo ordine, potenti quanto l'aritmetica di Heyting al secondo ordine, e finire quindi con calcoli estremamente potenti che considerano insieme entrambi i sistemi di tipi ed eventualmente anche i tipi induttivamente generati, i tipi ricorsivi ed i tipi intersezione. 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.

L' accertamento di profitto avverrà con una prova orale dopo il completamento di esercitazioni personali da parte dello studente.

L'esame intende valutare le conoscenze acquisite dallo studente sui temi del corso e le sue capacità di svolgere del lavoro autonomo su di essi.

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. : Oxford University Press,

Appunti forniti dal docente