Tesi

Computazione esatta sui numeri reali

La computazione esatta permette di 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. Questa materia può essere affrontata dal punto di vista teorico tematica ma sono anche state sviluppate diverse implementazioni, sia nella forma di librerie che impelementano in maniera esatte le funzioni fondamentali dell'analisi, sia all'interno di ambienti per il calcolo quali Mathematica.
Su questo argomento è possibile svolgere una tesi teorica o applicativa. Per fare degli esempi: dal punto di vista applicativo si possono sviluppare implementazioni della computazione esatta su GPGPU.. 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.