Logica in Informatica: dimostrazioni, tipi e computazioni

Starting date
January 1, 2002
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Masini Andrea
Keyword
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.

Sponsors:

Funds: assigned and managed by the department

Project participants

Andrea Masini
Full Professor
Publications
Title Authors Year
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

Activities

Research facilities