Matita e' un tool sperimentale di supporto alla dimostrazione interattiva di teoremi, in via di sviluppo al Dipartimento di Scienze dell'Informazione della Universita' degli Studi di Bologna.

Matita si fonda su di un Sistema di Tipi Dipendenti noto con il nome di Calcolo delle Costruzioni Induttive.

Questo calcolo integra al proprio interno alcuni cosrtutti computazionali tipici dei linguaggi di programmazione funzionali: in particolare, si possono definire funzioni per ricorsione (ben fondata), la cui applizazione puo' essere effetivamente calcolata come per normali programmi.

Al tempo stesso, le dimostrazioni sono una parte integrale del formalismo, cosa che permette di ottenere, attraverso l' isomorfismo di Curry Howard , una efficace integrazione tra specifica e ragionamento: le prove sono oggetti di prima classe del linguaggio e possono essere trattati come dei normali tipi di dato, inducendo in modo naturale uno stile di programmazione simile al proof-carrying-code, dove frammenti di software sono arricchiti con dimostrazioni di alcune delle loro proprieta'.

Matita e' attualmente adottato nel Progetto Europeo CerCo (Certified Complexity) per la verifica formale della preservazione della complessita' durante la fase di compilazione da linguaggio C verso un linguaggio assembly tipico di microprocessori per sistemi embedded.