Logica in Informatica: dimostrazioni, tipi e computazioni

Data inizio
1 gennaio 2002
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Masini Andrea
Parole chiave
Teoria della dimostrazione, Teoria dei tipi, Normalizzazione

La teoria della dimostrazione si e' rivelata di particolare importanza in informatica.

Un esempio notevole della stretta connessione tra informatica e teoria della dimostrazione e' dato dal cosiddetto isomorfismo di Curry-Howard il quale identifica le dimostrazioni in logica intuizionista con programmi, le formule dimostrabili con i tipi dei programmi e il processo di normalizzazione delle prove con le computazioni. Nel contesto dell'isomorfismo di Curry-Howard la Logica Lineare si e' rivelata di fondamentale importanza. La caratteristica principale della Logica Lineare e' quella di essere una logica costruttiva capace di esplicitare e controllare informazioni normalmente nascoste nelle logiche tradizionali (classiche e intuizioniste).
In questo progetto ci proponiamo di continuare lo sviluppo della Logica Lineare per permettere un controllo fine della complessita' di processi di calcolo.

Un altro notevole campo di applicazione e studio della logica in informatica e' dato dall'utilizzo di logiche modali e temporali per la specifica e la prova di proprieta' di sistemi complessi (concorrenti, mobili e distribuiti). Purtroppo, a causa della mancanza di una accettabile teoria della dimostrazione, l'utilizzo delle logiche temporali e' stato fortemente limitato a quei campi di applicazione per i quali si sono rivelati adeguati strumenti orientati ai modelli.
All'interno del progetto di ricerca intendiamo iniziare uno studio delle logiche temporali dal punto di vista della teoria della dimostrazione al fine di ottenere adeguati sistemi di prova classici ed intuizionisti.

Partecipanti al progetto

Andrea Masini
Professore ordinario
Pubblicazioni
Titolo Autori Anno
Towards a Formal Pragmatics: An Intuitionistic Theory of Assertive and Conjectural Judgements with an Extension of Goedel, McKinsey and Tarski's S4 Translation G. Bellin 2002
Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic G. Bellin; V. De Paiva; E. Ritter 2001

Attività

Strutture