Le strutture, le metodologie, le procedure dell'informatica, se prescindiamo dai dettagli della loro implementazione, sono nate dalla teoria logica della computazione, sviluppata a partire dagli anni 1930 (da Turing, Church, Post, Herbrand, Goedel...) e continuano a svilupparsi insieme ad essa. Un miracolo compiuto dall'ingegneria nel XX secolo (a partire da Turing, von Neumann, McCarthy,...) e` appunto l'aver permesso l'implementazione di tali strutture, metodi e procedure in tutta la loro generalita`. La rivoluzione nella logica che ha permesso questo incontro e` la considerazione del concetto dinamico di computazione effettiva, in aggiunta a quello di verita` tra le nozioni fondamentali della disciplina. Gli sviluppi vertiginosi della matematica computazionale, con l'uso di metodi algebrici, analitici e geometrici sempre piu` raffinati, non sono meno sorprendenti degli sviluppi ingegneristici, che portano a considerare i fenomeni computazionali facendo astrazione dal mezzo fisico (elettronico, biologico,...) in cui si realizzano.
Se il modello computazionale delle Macchine di Turing e` il piu` noto e generalmente usato in teoria della computabilita` e della complessita`, quello del lambda calcolo consente di illustrare in modo piu` diretto e sorpendente la corrispondenza fra deduzione logica e computazione, in particolare grazie alla corrispondenza di Curry-Howard tra proposizioni della logica intuizionistica e tipi del lambda calcolo, e tra deduzioni intuizionistiche e lambda termini (propositions-as-types). Sorprendente e` il fatto che uno stesso oggetto possa essere letto al tempo stesso come deduzione logica e come soggetto di un processo di computazione. Il fatto stesso che nessuno sappia in modo certo e definitivo come estendere questa corrispondenza dalla logica intuizionistica alla logica classica mostra che questo argomento di ricerca e` lungi dall'essere esaurito.
La relativa novita` delle idee e delle tecniche della logica computazionale permette di passare abbastanza presto dall'esposizione dei concetti fondamentali alla introduzione di argomenti avanzati, almeno dove ne esistano presentazioni eleganti e matematicamente mature. Questo corso consiste di tre moduli:
Tutti e tre i moduli consistono di una parte introduttiva, di circa 12 ore di lezione ciascuno e di una scelta di argomenti avanzati. Indichiamo qui sotto una lista di argomenti avanzati; solo alcuni di questi verranno presentati in classe, altri potranno costituire il tema di presentazioni da parte degli studenti. E` anche allo studio la possibilita` di tenere nell'AA 2004-5 un corso di dottorato in parallelo al presente corso, che coprirebbe appunto alcuni degli argomenti avanzati.