Home » Archivo » Archvio 2013 » FONDAMENTI LOGICI DEI LINGUAGGI FUNZIONALI - 2013/2014

Laurea Magistrale

Salta il menu di secondo livello

FONDAMENTI LOGICI DEI LINGUAGGI FUNZIONALI - 6 CFU - A.A. 2013/2014

Insegnante

Prof. Silvio Valentini

Periodo

I Anno - 1 Trimestre | 01/10/2013 - 07/12/2013

Ore: 48 (8 esercitazione, 40 lezione)

Torna su ▲

Prerequisiti

Conoscenze di base di logica matematica e del linguaggio insiemistico

Conoscenze e abilità da acquisire

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

Modalità di esame

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

Criteri di valutazione

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.

contenuti

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.

Attività di apprendimento previste e metodologie di insegnamento

Lezioni frontali in aula

Eventuali indicazioni sui materiali di studio

Appunti forniti dal docente

Testi di riferimento

Torna su ▲