Le logiche non classiche e le teorie dei tipi si sono dimostrate uno strumento efficace nella specifica formale e verifica di programmi, come
testimoniato dalla vasta letteratura. I proponenti hanno gia' ottenuto risultati nelle seguenti aree:
logica intermedie costruttive e specificazione di sistemi modulari [Lau&al04,Ferrari&al03], trattamento dell'informazione incerta mediante
logiche polivalenti [Aguzzoli&al05], teoria dei tipi sia dal punto di vista semantico mediante l'utilizzo di metodi categoriali [Bucalo&al03,Bucalo&al05], sia negli aspetti connessi alla dimostrazione automatica [Momigliano&al03,Beringer&al04].
La ricerca si propone di approfondire e sviluppare le linee di ricerca sopra esposte. In particolare si intendono conseguire i seguenti obiettivi:
(a) Logica costruttiva nelle specifica e validazione di sistemi OO. Si intende utilizzare una logica intermedia costruttiva studiata in
precedenza dai proponenti nella progettazione di un linguaggio di modellazione e specifica orientato agli oggetti.
(b) Studio di semantiche algebriche per una gerarchia di logiche polivalenti basate su T-norme. Lo scopo è l'individuazione di criteri guida per il loro utilizzo nella rappresentazione di sistemi in presenza di incertezza.
(c) Descrizione di categorie di modelli in termini delle nozioni algebriche di comonoide e omomorfismo di comonoidi. In particolare si
studieranno possibli estensioni dei risultati ottenuti alla teoria dei domini.
(d) Teoria dei tipi nella dimostrazione e verifica. Si studieranno framework più espressivi, orientati alla specifica e verifica di codice mobile, in particolare per quanto riguarda aspetti di consumo di risorse.