In search of bugs in computer programs

Jacopo Emmenegger received his doctoral degree in mathematics from Stockholm University in 2019. Thanks to a grant from Knut and Alice Wallenberg Foundation, he will hold a postdoctoral position with Professor Giuseppe Rosolini at the University of Genoa, Italy.

As we now increasingly rely on computers, how should we be able to judge if the software is correct? In order to verify the computer programs, new tools are being developed within mathematical logic. One system to ensure that the computer program does what it is intended to do is Dependent Type Theory, which was introduced in the 1970s by the Swedish logician Per Martin-Löf.

The first type theory was developed well before the time of computers, in the early 1900s by the British mathematician and philosopher Bertrand Russell. In his attempts to create common foundations for all mathematics, he encountered paradoxes, including the famous Russell paradox; in a classic version of it, a man from Crete says that everyone from Crete always lies. 

Later, the type theories developed into strictly formal systems useful for, among other things, studying programming languages. However, Dependent Type Theory is rather complicated to manage. A step to make it easier to handle was taken about ten years ago, when prominent mathematician Vladimir Voevodsky extended the dependent type theory with a new principle – the univalence axiom. For this axiom to be useful for verifying computer programs, its computational content must be investigated.

Using so-called realisability models, Jacopo Emmenegger will test in his project to what extent the univalence axiom is computable. The realisability models are based on an abstract version of Turing machines, the earliest and most studied calculation models. Turing machines can be seen as a collection of instructions for reading and writing ones and zeros on a strip, making them an abstract version of modern computer programs. 

To be able to determine whether calculations can be performed with the dependent type theory extended by the univalence axiom, one has to find a realisability model where each term in the type theory corresponds to a Turing machine. At the same time, the project combines two of the most important methods in computer programming: type theory and realizability.

Photo: Ota de Leonardis