1. Dispense del docente (online);
2. A.S. Troelstra, H. Schwichtenberg, Basic proof theory, Cambridge University Press 1996;
3. J.R. Hindley, J. Seldin, Lambda-Calculus and Combinators, an Introduction, Cambridge University Press 2008.
Obiettivi Formativi
l corso si propone di fornire agli studenti la conoscenza delle principali problematiche e metodologie della teoria strutturale della dimostrazione (relativamente alla logica classica e intuizionistica e ad alcune logiche sottostrutturali), nonché una introduzione alle principali teorie delle operazioni (logica combinatoria, lambda calcolo, lambda calcolo tipato) e alla corrispondenza Curry-Howard.
Prerequisiti
Il corso propedeutico da 12 CFU di Logica (CdS triennale), o conoscenze equivalenti (in questo caso parlare con il docente prima dell'iscrizione al corso).
Metodi Didattici
Lezioni frontali (+ esercitazioni)
Altre Informazioni
.
Modalità di verifica apprendimento
Esame orale
Programma del corso
(i) Introduzione e complementi di logica proposizionale e predicativa;
(ii) calcoli delle sequenze (L-calcoli di Gentzen; calcoli di tipo G3) per la logica classica e intuizionistica elementare;
(iii) teorema di eliminazione delle cesure e principali applicazioni (es.: lemma di Maehara e interpolazione; teorema di Herbrand);
(iv) cenni alle logiche sottostrutturali (in particolare logica lineare affine e logica lineare);
(v) logica combinatoria e lambda-calcolo non tipato; teorema di Church-Rosser e sue applicazioni; teorema del punto fisso e sue applicazioni.
(vi) lambda calcolo tipato; normalizzazione; corrispondenza di Curry-Howard.