In May 2006, on the Plateau de Saclay, about 20 kilometers south of Paris, three research projects in the fields of formal methods and security were launched at the brand-new, Orsay-based Microsoft Research-Inria Joint Centre.
The lab, founded by the Institut National de Recherche en Informatique et en Automatique (Inria)—the French National Research Institute for Computer Science and Applied Mathematics—along with Microsoft and Microsoft Research Cambridge and officially inaugurated on Jan. 12, 2007, established as its objective the pursuit of fundamental, long-term research in formal methods, software security, and the applications of computer-science research to the sciences.
Alternatively, you could consider the innovative software and tools designed and implemented, in research areas as diverse as mathematics, image and video mining, and secure distributed computing―all available for download by the research community.
At 5:46 p.m. on Sept. 20 2012, Georges Gonthier, principal researcher at Microsoft Research Cambridge, sent a brief email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris. It read, in full:
“This is really the End.”
Those five innocuous words heralded the culmination of a project that had consumed more than six years and resulted in the formal proof of the Feit-Thompson Theorem, the first major step of the classification of finite simple groups.
The theorem, first proved by Walter Feit and John Griggs Thompson in 1963 and also known as the Odd-Order Theorem, states that in mathematical group theory, every finite group of odd order is solvable.
That might seem a deceptively simple definition to non-mathematicians, but Gonthier and his collaborators on the Mathematical Components project at the Microsoft Research-Inria Joint Centre are anything but. Their achievement in completing a computer-assisted proof by the Coq proof assistant, developed at Inria, , was acclaimed widely as news spread.
Andrew Blake, laboratory director at Microsoft Research Cambridge, provided further detail:
“Georges and his team at Inria have been working on this proof of the Feit-Thompson or Odd-Order Theorem for six years or so, since he completed his proof of the Four-Color Theorem. That might seem a long time for one theorem, but in fact:
“One may anticipate that this could affect profoundly both computer science and mathematics.”
Then there is the research personnel involved:
No matter how you look at it, the Microsoft Research-Inria Joint Centre―an extension of an informal but long-term relationship between two giants of European computer science, the late Roger Needham, founding director of Microsoft Research Cambridge, and the late Gilles Kahn, then Inria chairman―has proven a resounding success.
Michel Cosnard, Inria chairman and chief executive officer, concurs―and regards the Joint Centre as the natural extension of a proud tradition.
“European research and education have always been excellent in theoretical computer science and mathematics, in particular in France,” Cosnard says. “By grounding our collaboration in our strengths and expertise and by exploring promising challenges, Microsoft researchers and Inria researchers open new avenues in computer programming and software production―and provide new tools for scientists in other disciplines to progress.
“The results are already impressive. But what is most impressive is the quality of the relationships between Microsoft Research and Inria researchers: full respect, trust, and confidence.”
The path to the creation of the Joint Centre began in April 2005, with the signing of a memorandum of understanding by François d’Aubert, French secretary for Research; Kahn; and Steve Ballmer, Microsoft chief executive officer. In October of that year, François Goulard, French minister of Higher Education and Research, joined Kahn and Microsoft Chairman Bill Gates in signing a framework agreement. The new lab was established near the campus of Inria Saclay.
Under the direction of leading Inria researcher Lévy and with strong political support from the French government, the Joint Centre operates on a model of equally shared investment. Inria provides space and infrastructure. Microsoft France helps with administration and public relations. Researchers from both Microsoft Research and Inria make visits ranging from a week to years. Inria hires post-docs and Ph.D. to staff projects led collaboratively by researchers from both Microsoft Research and Inria.
In addition, all intellectual property created by the Joint Centre is jointly owned. Both Inria and Microsoft Research have equal exploitation rights to the intellectual property created. And, as noted, the lab is strongly committed to open publication and community software.