L'insegnamento è organizzato come segue:

Obiettivi formativi

Modulo: LOGICA
-------
Il corso si propone di introdurre la logica matematica e di chiarire come essa sia ausiliaria alle altre materie. Temi centrali sono la distinzione tra sintassi e semantica, la formalizzazione di proprietà nel linguaggio logico e il concetto di dimostrazione corretta, basata su regole generali prefissate. Verranno presentate tecniche per produrre prove e contro-esempi.


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
-------
Livelli di riferimento. Linguaggio e meta-linguaggio.
Logica proposizionale e predicativa (classica e intuizionista).
Introduzione del calcolo dei sequenti con equazioni definitorie.
Sistemi LJ e LK. Teorema di eliminazione dei tagli. Ricerca delle prove.
Interpretazione classica delle formule, sia proposizionale che predicativa.
Teoremi di Correttezza, Completezza e Compattezza per il calcolo LK.
Problema della decisione per il calcolo predicativo.
Teoremi di incompletezza.


Modulo: LINGUAGGI
-------
Induction:
(i) Mathematical induction over the natural numbers;
(ii) Structural induction;
(iii) Rule induction.
Operational semantics:
Big step and small step semantics for simple languages including
• Exp, Bool, languages for arithmetic and Boolean expressions
• the imperative language of while commands While
• the functional languages Fun and Lambda and simple variations on them; call-by-name and call-by-value semantics.
Typing:
(i) Typing assignments for the languages Fun and Lambda
(ii) Progress and preservation.
(iii) For Lambda you should be familiar with the computational consequences of using types; in particular the need for explicit fixpoint operators.

Bibliografia

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.