Inria Prize

Gilles Dowek: an explorer of formal methods

Changed on 05/12/2023
Gilles Dowek, Inria director of research and guest professor at ENS Paris-Saclay, has his sights set on devising mathematical proofs which can be used in all countries and with all systems. The author of a large number of papers on formal methods and guided by universalist utopias, Dowek has had a rich and varied career, for which he has just been awarded the Inria - French Academy of Sciences Grand Prize.
Portrait de Gilles Dowek
© Inria / Photo B. Fourrier

Developing an “Esperanto” for formal methods

Gilles Dowek, head of the Deducteam project team at the Inria Saclay Centre and guest professor at ENS Paris-Saclay, is seeking to create an Esperanto for proof verification systems (also known as proof assistants) which, like the Coq assistant developed by Inria, are used to verify mathematical proofs. Coq – which Dowek made a brief contribution to early on in his career – is one of the proof verification systems to have been recognised by the ANSSI (the French cybersecurity agency). It is used to rigorously demonstrate that a product verifies a certain property, e.g. that it is not vulnerable to a certain type of cyberattack.

Now 56, Gilles Dowek has spent a large chunk of his career on these formal methods.  A devotee of philosophy, this graduate of the École Polytechnique was previously awarded the Philosophy Grand Prize by the Académie Française in 2007 for his book Les métamorphoses du calcul, une étonnante histoire des mathématiques (published by Le Pommier). “My primary ambition is philosophical: to come up with a definition for the concept of a mathematical proof - a rare anthropological invariant - that can be used in all countries and with all systems.” In recognition of his remarkable career, Gilles Dowek has been awarded the Inria - French Academy of Sciences Grand Prize. “I have a great deal of respect for this award, which carries a lot of weight and helps to promote scientific discoveries within the wider society.”

Brief biography

  • 1988: graduates with a bachelor’s degree from the École Polytechnique.
  • 1991: PhD at Paris 7 University on automated theorem proving in the calculus of constructions.
  • 2000: winner of the Prix d'Alembert des Lycéens, awarded by the French Mathematical Society for his work in popularising science.
  • 2000-2010: head of the Logical project team.
  • 2010: the project team Deducteam is created.
  • 2011: part of a group of experts put together by the French Ministry of National Education to develop curricula for IT and digital science for pupils in their final year of high school.
  • 2021: appointed to France’s national digital council.
  • 2023: appointed to France’s high council for curricula as a qualified personality.

One of the challenges Gilles Dowek is seeking to address is the vast array of different proof verification systems used across the world. “When working on the development of Coq early on in my career, I found myself thinking about the wide range of languages created for Coq and other comparable systems, such as Isabelle (developed in Germany), HOL Light (developed in the UK), PVS and Lean (developed in the USA) or Mizar (developed in Poland). Around twenty or so proof languages are currently in use, which creates issues with regard to universality and sharing. The concept of mathematical truth is an anthropological universal that we must strive to preserve, making sure that proofs can be read everywhere.” 

In response to these challenges, Gilles Dowek and the researchers from Deducteam analysed the construction and the theoretical foundations of different proof languages currently in use (a form of lambda calculus for Coq). “We developed a new logical framework, Dedukti (which means "to deduce” in Esperanto), for expressing common logics and theories for different systems. The main features of each proof assistant are translated into Dedukti.” This process has some highly practical applications: the team has translated both the formal specification language TLA+, which is widely used in industry, and the B method, which is used by the RATP (the public transport operator in Paris) to verify any corrections made to the software used on a number of automated metro lines.

Developing transportable proofs capable of being used over and over again

This work has been extremely rewarding for Gilles Dowek, providing him with some unforgettable moments at both a collective and a personal level.

One of my happiest memories goes back to an article I wrote pretty much in one night back in August 2006. That article was crucial to the development of Dedukti, and it was like everything just came together: I had been stuck for weeks, then I came up with this very simple idea and my proof started to work really smoothly.

The next step will be to make it easier to translate proofs generated by individual systems and share them with composite systems such as B or TLA+, which use different “external provers” for verification. “Translations make sharing safety and security proofs easier and quicker, and are demanded by national cybersecurity agencies.  In France, the ANSSI requires proofs to be in either Coq or B, while its German equivalent, the BSI (Bundesamt für Sicherheit in der Informationstechnik) prefers proofs in Isabelle.” 

Dedukti is now being used by a growing number of international users, in countries such as Japan, Brazil, Israel and the USA, underlining the potential of this logical framework. This is also testament to all of the hard work put in by Gilles Dowek and his colleagues from Deducteam.

Scientific Prize Inria - French Academy of Sciences

Discover the winners of the 2023 edition! Inria - French Academy of Sciences Grand Prize

Bringing science to the people through a multidisciplinary approach

Straddling the worlds of research and society, Gilles Dowek has rubbed shoulders with many philosophers, including Michel Serres, as well as figures from the world of education. He was co-author of a report by the French Academy of Sciences on the teaching of computer science in 2013 and has been a member of France’s high council for curricula since 2023.

Committed to reaching out to the wider public, Gilles Dowek particularly enjoys meeting up with school pupils and university students, something he feels to be essential. “There is a risk of science being confined to a peripheral social function, when it ought first and foremost to be something that is shared. As researchers, meeting the public in this way forces us to regularly question our choices and the directions we go in.” 

Find out more

For the general public:


For experts: