Getting more than one ERC Advanced Grant in a lifetime is something that extremely few have accomplished. Thierry Coquand, Professor at the Division of Computing Science, Department of Computer Science and Engineering at Chalmers and University of Gothenburg, got his first ERC Advanced Grant for his work in 2009.
Thierry Coquand on his research – and now receiving the ERC grant twice:
“The topic of my research is about representation of mathematical proofs on a computer. This is used to design so called "proof assistants” that help a mathematician and/or a computer scientist to build a mathematical proof, in particular, ensuring that the proof is correct.
There has been a growing use of such system for checking and documenting complex software systems, but also mathematical proofs. One aspect of this research that I find particularly interesting is that trying to represent mathematics on a computer forces us to think about the nature of mathematical objects.
While I was working on my previous ERC project, it was realised by a great mathematician, the late Vladimir Voevodsky, that the language we were using for the representation of proofs on a computer was actually well adapted to express recent abstract concepts in mathematics, connected to the notion of homotopy, which is a general study of the notion of “shapes”. This was both surprising and exciting, and the present project should explore further these connections.
I believe that this field of research is important both for society, given that the issues of software correctness and security are crucial, and because of its intrinsic logical interest. If successful, this project will create proof assistants that can help in the development of sophisticated mathematics and highly modular pieces of software.
This work is really a team work – both local and internationally. It is really nice, and not so common, to be part of a team which have strong competence both in theory and in the actual implementation of proof assistants. I also want to thank the people at the Grants Office, in particular Maria Enge, for all their help.”
More on Thierry Coquand's research:
Research on interactive proof systems receives funding from KAW
Watch the webinar: Hydrogen – A silver bullet in the energy system?
