Foto del docente

Claudio Sacerdoti Coen

Professore associato

Dipartimento di Informatica - Scienza e Ingegneria

Settore scientifico disciplinare: INF/01 INFORMATICA

Coordinatore del Corso di Laurea in Informatica

Temi di ricerca

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.