Research on interactive proof systems receives funding from KAW
Checking that software in computers is calculating correctly is very difficult. Thierry Coquand, professor in the Logic and Types division at Computer Science and Engineering, receives SEK 35 million from the Knut and Alice Wallenberg Foundation for a project on systems that help to check the correctness of mathematical reasoning, so-called interactive proof systems.
"The trick is to use software to verify software. The basic idea is to consider programs, their inputs and outputs, as mathematical objects and ask a mathematically exact question about their accuracy," says Thierry Coquand.
The method has been used successfully when it comes to controlling software used in, for example, avionics.
According to Thierry Coquand, the need for this type of control is also beginning to be felt in pure mathematics. The reason is that the length and complexity of mathematical proofs has increased.
"Two examples are Feit-Thompson's theorem of more than 250 pages and the four-color theorem, the proof of which was impossible to carry out by hand. Both proofs has now been verified by interactive proof systems."
Thierry Coquand's project is based on theories formulated by the Russian-American mathematician Vladimir Voevodsky. A decade ago, he became increasingly concerned about the complexity of proofs in his own research.
"His new way of looking at mathematical objects has pioneering consequences for the foundations of mathematics, and in the design of interactive proof systems," says Thierry Coquand.
The project "Type Theory for Mathematics and Computer Science" receives funding of SEK 34,700,000 over five years. It will be a collaborative project between computer scientist Thierry Coquand at University of Gothenburg and mathematician Peter Lumsdaine at Stockholm University.
A total of 18 research projects have been granted a total of SEK 541 million by the Knut and Alice Wallenberg Foundation.
Text: Thomas Melin