Parole chiave:
Teoria dei tipi
Dimostrazione assistita
Mathematical knowledge management
Lambda-calcolo
Linguaggi di programmazione
Smart contracts
Progetta e implementa Matita (http://matita.cs.unibo.it), uno
strumento di supporto alla dimostrazione interattiva di teoremi.
Coordina un progetto europeo per lo sviluppo e la certificazione di
un compilatore per C che rispetti la complessita' computazionale e
computi annotazioni di costo esatto. Ha coordinato un Progetto
Strategico per la valorizzazione del nucleo di Matita per la
realizzazione di strumenti di e-learning per l'apprendimento
interattivo di tecniche di dimostrazione in Analisi I. Studia il
Mathematical Knowledge Management di librerie distribuite di prove
matematiche formali, con particolare attenzione alla ricerca di
risultati nella libreria e alla loro rappresentazione tramite
ricostruzione di rappresentazioni linguistiche adeguate. Studia
algoritmi efficienti per il parsing e l'interpretazione semantica
di linguaggi tipati fortemente ambigui, quali l'usuale notazione
matematica. Studia la corrispondenza fra linguaggi tipati
Curry-Howard isomorfi a logiche classiche, linguaggi dichiarativi
per prove matematiche e OMDoc, lo standard de facto per la
rappresentazione di documenti matematici in formato XML.
