Tesi

Computazione esatta sui numeri reali

Questa tematica studia metodi per effettuare i calcoli sui reali con una precisione arbitraria, senza che nessuna cifra fornita come risultato sia affetta da errore. Si evitano così alcuni degli svantaggi insiti nella tradizionale computazione floating point. Recentemente nella comunità scientifica c'è stato un aumento di interesse su questa materia e diverse applicazioni pratiche sono stata sviluppate.
Su questo argomente sono possibili tesi sia teoriche che applicative o di rassegna. Per fare degli esempi: dal punto di vista applicativo si possono testare e sviluppare ulteriormente alcune applicazioni della computazione esatta. Da un punto di vista teorico si possono sviluppare dimostrazioni di correttezza per algoritmi sui numeri reali, oppure studiare i vari formalismi per la definizione delle funzioni computabili.

Sistema per la dimostrazione formale assistita

Questi sistemi, di cui Coq è un esempio, permettono lo sviluppo assistito ed interattivo di dimostrazioni matematiche. Nelle applicazioni pratiche questi sistemi permettono di garantire la correttezza dei programmi. La ricerca su questi argomenti è piuttosto attiva e tesi in questo campo possono andare sia nella direzione dello studio teorico sia nella sviluppo pratico di dimostrazioni formali in ambiti diversi.

Linguaggi di programmazione

In questo ambito si studiano metodi formali per definire le specifiche dei linguaggi di programmazioni, e dimostrare la correttezza dei programmi.