European Research Council 2011
Dale Miller: “Making proof universal”
Â© Inria / Photo Kaksonen
As the beneficiary of an ERC Advanced Grant for experienced researchers, Dale Miller has embarked on the difficult path of establishing proof. His aim? In this field, which is highly abstract but which has a definite impact on the real world, he wishes to standardise proof systems and issue certificates for such systems in order to promote greater confidence in them.
One thing of which Dale Miller is convinced is that the securing of ERC funding is going to help both him and Parsifal, his project-team, make significant progress along the long path towards proof. And this progress is set to benefit everyone! This proof is somewhat akin to the Holy Grail for computer-science and mathematics researchers. How can it be proved that a software program or an electronic circuit does exactly what is expected of it, and that it does so under the conditions and in compliance with the specifications that presided over its creation? To prove the validity of a program featuring several million code lines, it is sometimes necessary to design a new program, itself composed of several hundred thousand code lines…
It is a subject that is far from trivial. Digital systems are multiplying in number, and not just in the fields of leisure activities or entertainment, where the user can restart the system themselves in the event of an error, or manage without a particular function if it is affected by a bug. Today, codes and programs guide, control and automate many tasks that have an impact on our daily lives, and that cannot tolerate malfunctioning of any kind. The launch of a rocket that is to release a communications satellite supposed to work autonomously for fifteen or so years must be made 100% reliable. Likewise, in the monitoring of the temperature of an incubator or the heart rate of a patient who has just undergone heart surgery, there is no room for faults. Not to mention airliners, bank transaction systems, telecommunications, etc. In addition, there is the question of security: how can we protect all of these digital objects from viruses and malicious attacks?
Dale Miller has been working on these subjects for quite some time. After achieving a Ph.D. in mathematics at the university of Carnegie Mellon, he became a computer-science professor and researcher. He first worked in the United States, and then in Europe, where his subject, computational logic, has met with great interest within research circles. He was particularly attracted by the cities of Edinburgh, Glasgow, Genoa, Pisa and Siena, but it is in France that he has finally settled. An American married to an Italian, he moved to the Paris region in 2002 when he took on the roles of senior research scientist at the Inria Saclay centre and professor at the Ecole Polytechnique. His level of French does not quite measure up to his commitment to French research, “I’d have to leave the lab if I wanted to speak French properly”, he says. It is true that he is surrounded by a very cosmopolitan team on a daily basis: a German, an American, an Indonesian, Dutch, Italians... and French nationals, and that in research the working language remains English!
The idea is to create a market place where it will be possible to exchange and share the proof systems developed in different locations.
He mentions the Tower of Babel, not in reference to the multilingualism of his environment, but rather to describe the situation as regards proof. “No standard exists within this field. Every time proof is needed that a system works, a budget and a student are required in order to develop a verifier of the system's property proofs. Moreover, this verifier is designed on an ad hoc basis and functions for a single system only. At times it does not even work for the subsequent version of the same system!” The most explicit counter example is that of text files: “ever since the invention of html language, it has been possible for files to be read by any browser. This is what we wish to achieve within the field of proof.”
His idea: to perform “computer-science chemistry”, that is, use the atoms of existing inferences to develop molecules of inferences. In other words, to offer certified proof-system modules in order to be able to compose an arbitrary system... “The idea is to create a market place where it will be possible to exchange and share the proof systems developed in different locations.” In order to achieve this, Dale Miller envisages issuing “proof certificates”; this is the purpose of the ProofCert project that won him the ERC grant. “The subject is actually very abstract, but it has a definite impact on the real world and on our lives...”
ProofCert, certifying proof!
Dale Miller spent three years fine-tuning the ProofCert project within different symposiums and with funding agencies before being awarded the ERC Advanced Grant, worth 2.2 million Euro for a period of five years as of January 2012. In concrete terms, this will enable the recruitment of PhD students and post-doctoral researchers and the invitation of numerous researchers within the field.
In short, ProofCert aims to standardise proof systems, certify them, index them in a library and make them available on a market place. “The idea is to instil confidence in existing proof systems so that people can discuss and share their work in these domains”, explains Dale Miller, “rather like in the field of viruses and anti-viruses, which is very dynamic and very cooperative today”.
Successful applicants 2011
In the "Young researchers" category, Remi Gribonval (Metiss, Rennes), Andreas Enge (Lfant, Bordeaux), Xavier Rival (Abstraction, Rocquencourt) and Erwan Faou (Ipso, Rennes) received a grant, which will enable them to build a team. In the "senior researchers" category, the projects by Marie-Paule Cani (Evasion, Grenoble), Nicholas Ayache (Asclepios, Sophia Antipolis) and Dale Miller (Parsifal, Saclay) were those selected by the ERC.
2011 successful applicants
Â© Inria / Photo Kaksonen
"make 3D virtual creation available to all"
Â© Inria / Photo Kaksonen
“Making proof universal”
"Computational tools serving mathematics"
Erwan Faou - Ipso project-team
« Mathématicien du son et de l’image »