Il gruppo si colloca all’interno dell’area dei Metodi Formali dell’Informatica e si occupa delle seguenti tematiche di ricerca.

Logical Frameworks e ambienti interattivi per il ragionamento formalizzato. L’obiettivo di questa linea di ricerca è sviluppare la teoria e sperimentare l’implementazione di ambienti interattivi (editors), che possano assistere gli utilizzatori di metodi logico-formali per la certificazione e lo sviluppo di software. I Logical Frameworks considerati sono tutti basati sulla Teoria Costruttiva dei Tipi, e quindi sulle analogie delle formule-come-tipi e dei giudizi-come-dimostrazioni, sviluppata da Martin-Lof e da Plotkin-Harper-Honsell negli anni ’80. La loro teoria LF, fu il primo metalinguaggio per derivazioni formali direttamente implementabile e per questo ricevette il IEEE Logic in Computer Science Test-of-Time Award nel 2007. Negli ultimi 30 anni il settore è molto cresciuto e il gruppo di ricerca di Udine ha pubblicato oltre 50 lavori ed è sempre stato uno dei membri di riferimento nel network europeo TYPES. Il più recente obiettivo di ricerca del gruppo è l’implementazione di LLFP, un Logical Framework che permette di prototipare rapidamente, ma in modo assolutamente trasparente, utilizzando il meccanismo delle monadi, editors specifici per logiche dei programmi complesse. Ovvero quando le logiche utilizzano evidenza esterna non formale proveniente da fonti eterogenee oppure presentano vincoli (side conditions) arbitrari sulla forma delle derivazioni. Un primo prototipo del type checker di LLFP è stato recentemente implementato in OCaml da Vincent Michielini dell’ENS di Lione nell’ambito di uno stage di ricerca che ha visto anche la collaborazione scientifica di Luigi Liquori dell’INRIA di Sophia Antipolis.

Il gruppo si è anche impegnato nell’adattare a nuovi aspetti computazionali le capacità di sintesi dei logical frameworks basati sulla teoria dei tipi. In particolare, sfruttando l’isomorfismo di Curry-Howard è stata sviluppata una metodologia per sintetizzare programmi distribuiti Erlang certificati, a partire da dimostrazioni in Coq. Infine, si sono utilizzati opportuni logical frameworks (e.g. rewriting logic) per sviluppare nuove metodologie di verifica e analisi formale di sistemi concorrenti.

Modelli insiemistici e categoriali di oggetti infiniti. L’obiettivo di questa linea di ricerca è studiare modelli, sia insiemistici che categoriali, per catturare il comportamento di processi infiniti.