An academic from the University of Nottingham has been awarded a Consolidator grant from the European Research Council (ERC), worth €2 million, to further explore an area in the intersection of computer science and mathematics.
Dr Nicolai Kraus, from the School of Computer Science, will use the grant to develop connections between type theories, formal systems that certain computer programming languages are based on.
When computer programs fail or don’t work properly, type theories allow programmers to avoid software problems. Using mathematical languages, experts can use type theories to check mathematical reasoning and check for any mistakes in programming.
Computer errors of this type in the past have caused airplanes to crash and the failure of rocket launches, so the ability to prevent these mistakes and correct them is highly beneficial.
The Consolidator Grant will allow Dr Nicolai Kraus to enable different type theories, that understand different mathematical languages, to work together effectively. It is hoped that translations between these languages will help make the technology easier to use and enable the general population to benefit from it.
He hopes that the work supported by this ERC Consolidator grant will help researchers in the field to better benefit from each other’s results and reduce the amount of work that has to be replicated.
Whilst this project is funded for five years, Dr Kraus expects that deep underlying mathematical challenges will mean that there won’t be a simple single solution to the problem. Instead, he hopes to find a collection of results that can form the basis for further future developments in the sector.
He explained: “Type theories are systems that allow computers to check and assist with formal reasoning. We can use type theories to verify mathematical theorems, or to write computer programs that come with a proof of correctness, which means that the program is guaranteed to do exactly what its specification says.
“It is a vibrant field and it is absolutely impressive what people have achieved using type theories. But people have different preferences and priorities, which is why many different type theories are used today, and it is not always easy to transport work from one to another. This is exactly the issue that my team and I will try to resolve in this project, by constructing translations and finding connections between type theories."
The ERC selected 308 researchers for this year’s Consolidator Grants, where academics are pursuing the most promising scientific ideas.
President of the European Research Council Professor Maria Leptin said: “The new Consolidator Grant winners represent some of the best of European research. It is disappointing that we cannot support every deserving project simply due to budget constraints; around 100 proposals identified as excellent in our rigorous evaluation will be left unfunded. Can Europe afford to let such talent go unrealised?"
More information is available from Dr Nicolai Kraus on Nicolai.Kraus@nottingham.ac.uk
Read the full story here: https://www.nottingham.ac.uk/news/type-theories-erc-grant?dm_i=5IL5,XKLI,3Y4623,45IVI,1
Posted on Wednesday 6th December 2023