Studiare
In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.
Piano Didattico
Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.
1° Anno
Insegnamenti | Crediti | TAF | SSD |
---|
2° Anno Attivato nell'A.A. 2012/2013
Insegnamenti | Crediti | TAF | SSD |
---|
Tre insegnamenti a scelta tra i seguenti
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Tre insegnamenti a scelta tra i seguenti
Insegnamenti | Crediti | TAF | SSD |
---|
Legenda | Tipo Attività Formativa (TAF)
TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.
Fondamenti (2011/2012)
L'insegnamento è organizzato come segue:
Obiettivi formativi
Modulo: LOGICA
-------
Il corso si propone di introdurre la logica matematica. Verranno introdotti e approfonditi i principali metodi semantici (teoria dei modelli) e sintattici (calcolo dei sequenti) per la logica dei predicati del primo ordine.
Modulo: LINGUAGGI
-------
L'obiettivo del corso è quello di presentare le basi teoriche dei linguaggi di programmazione. A tale scopo verranno introdotti vari linguaggi sequenziali paradigmatici anche di ordine superiore. Tutto il corso sarà incentrato sui concetti di semantica operazionale e di sistema di tipo. Verranno introdotte alcune tecniche formali per la verifica del comportamento dei programmi.
Programma
Modulo: LOGICA
-------
Strutture e Linguaggio del Primo Ordine:
connettivi,variabili, quantificazione. Semantica di Tarski del linguaggio del primo ordine. Concetto di modello. Identità.
Teoria dei Modelli:
omomorfismi, equivalenza elementare, strutture e sottostrutture.
Teoria della dimostrazione:
Il problema dell’assiomatizzazione. Il calcolo dei sequenti LK. L'eliminazione del taglio. Proprietà della sottoformula e consistenza del calcolo puro dei predicati. Eliminazione del taglio per teorie matematiche del I ordine.
Semantica e Sintassi a confronto: Teroremi di correttezza, e completezza. Teorema di compattezza. Teoremi di Löwenheim-Skolem (Upward e Downward)
Modulo: LINGUAGGI
-------
Induzione:
(i) Induzione matematica sui numeri naturali;
(ii) Induzione strutturale;
(iii)Induzione su un sistema di inferenza.
Semantica operazione:
Semantica big step e small step per semplici linguaggi sequenziali, tra cui:
(i) Exp, Bool, linguaggi per espressioni aritmetiche e booleane.
(ii) Il linguaggio imperativo While dei comandi while
(iii)I linguaggi funzionali Fun e Lambda e loro variazioni; semantiche call-by-name e call-by-value.
Sistemi di tipo
(i) Assegnamenti di Tipo per i linguaggi Fun e Lambda
(ii) Le proprieta' di Progress and preservation.
(iii) Per il linguaggio Lambda lo studente dovra' conoscere le consequenze computazionali dell'uso dei tipi; in particolare la necessita' di usare operatori espliciti di punto fisso.
Modalità d'esame
Modulo: LOGICA
-------
Prova scritta.
Modulo: LINGUAGGI
-------
L'esame consiste in una prova scritta e una eventuale prova orale, a discrezione del docente.