Jasmin Blanchette awarded an ERC grant for his Matryoshka project
Changed on 26/03/2020
Jasmin Blanchette, a researcher on the VeriDis project team, based at Nancy and Saarbrücken, has won an ERC Starting Grant (StG) for his Matryoshka project. Success at his first attempt, which we look at in a good-humoured interview flavoured with a touch of poetry.
What exactly is your work about?
My work concerns interactive theorem proving, proof assistants. When we want to use a theorem, we must prove it first. It’s what mathematicians do all day long, but also computer scientists when they want to check that their algorithms and programmes are correct. Proof assistants (e.g. Coq and Isabelle) are software tools that we use to help develop mathematical proofs, enabling theorems to be proved in a very thorough manner. My work concerns both the development of this type of software and its use.
What attracted you to this field of research?
Piercing the mystery! It was a combination of circumstances that led me to the interactive proof field: during my bachelor’s degree, I took courses in formal proof and I naively told myself that a software tool could replace our paper-based proofs: I thought that was a great idea. What I did not know at the time was that this type of software already existed! When I went back to university for my master's, I joined the formal methods group. That’s where I discovered the existence of proof assistants, which was a revelation. When I finished my masters, I looked for a thesis supervisor working in the field of interactive proof systems; even though it was entirely new to me, I knew that I would enjoy it, and indeed that proved to be the case.
In life, we have to follow our impulses, more than our knowledge or our talents; we’re always at our best when we are motivated!
What is the purpose of the research that you proposed to the ERC?
In the field of theorem provers, there are two communities that are somewhat in opposition. There are researchers who do interactive theorem proving and those who prefer automated provers. For me, this distinction is rather artificial since we use automated proving in interactive, and even so-called automated tools need the user’s input. With my ERC project, I want to influence both communities. At Inria Nancy – Grand Est and Saarbrücken, we are lucky enough to have experts in both fields.
So my project aims to combine these two communities by developing automated proving systems but as applied to interactive proof assistants. Automated tools are powerful but restricted to less expressive logic while proof assistants offer richer logic and are generally more reliable but are less well automated. I would like to combine the advantages of the two types of software, while minimising their defects.
I propose a Russian doll approach, hence the name Matryoshka. It’s an ambitious project but it has been deemed feasible, in particular thanks to the local expertise that I can count on at Nancy and Saarbrücken.
What is the recipe for obtaining an ERC grant first time around?
You have to convince different people, whether they are experts in the field or not, that the project is coherent in its implementation and that all the steps you set out are necessary to moving the project forward. When you apply for an ERC grant, you have to think about communication. You must be able to explain the project clearly with a pleasant typeface and layout, and useful diagrams; you need to focus as much on the form of the project as on the content. Each word, like a rhyme in a poem, must move towards the purpose of the project as naturally as possible. That’s why it’s important to identify the principal problem correctly and end up with a process that solves it. The project must be comprehensible without effort on the part of the reader. At Inria, we are lucky enough to have excellent support. I had help from many colleagues, to whom I am very grateful. I would like to express particular thanks to my coach, Jean-Pierre Banâtre, for his very frank feedback.
And then, you have to believe in your project and in yourself. Only 10 % of applicants obtain an ERC grant. I said to myself that I had to propose a project that was clearly better than the others were; so I studied previous projects and I made sure that my text was more convincing. The project came into my head several months before I started writing it. It was a bit like the statue that a sculptor sees in a block of marble. The first ideas emerged in a restaurant while I was waiting for a friend. I still have the tablecloth I wrote them down on…
How will you use the funding?
The budget allocated to me will allow me to put together a team, hire some PhD students and engineers, pay for travel to conferences or invite other researchers here. It will be a team distributed between Nancy and Saabrücken to enable closer exchanges and co-operation. It will be a team that looks like me!
1997-2000 : bachelor in computer science at the University of Sherbrooke (Canada)
2000-2008 : software developer at Trolltech, a Norwegian company ( now called Qt Company)
2006-2008 : master in computer science at the University of Oslo
2008-2012 : PhD at the « Technische Universität München » (Munich)
2012-2014 : postdoctoral research at the Technische Universität München
January 2015 : researcher (starting researcher) at INRIA Nancy - Grand Est and guest researcher at the Max Planck-Institut für Informatik in Saarbrücken
