Highlights

Inria and Microsoft Research  Collaboration: a Joint Success

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.

How best to measure that progress? One method to attempt an assessment could be to examine the contributions to the greater research community:

  • papers published in academic journals, presented during prestigious conferences and workshops, or published as technical reports.
  • Participation in dozens of events, conferences, workshops, seminars, presentations, and invited talks.

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:

  • “It is a big theorem—the proof runs to two volumes. This is a large body of material to verify by eye—how much confidence can one have in that? Now the verification is substantially automated through the use of Coq.
  • “Along the way, a good deal of the structure of finite-group theory—textbooks of standard results—have been coded and verified.
  • “All of this has also stressed the Coq proof environment and strengthened it, and Coq is also used for a multitude of verification tasks in security-critical code.

“One may anticipate that this could affect profoundly both computer science and mathematics.”

Then there is the research personnel involved:

  • Inria has contributed researchers, a system engineer, and three lab directors, including Jean-Jacques Lévy, Inria research director, who headed the Joint Centre until September 2012 and Laurent Massoulié who took over him.
  • Microsoft Research has contributed researchers, and the lab’s deputy director, Pierre-Louis Xech, is from Microsoft France.
  • researchers from other French academic institutions are working on Joint Centre projects.
  • Ph.D. candidates have participated in Joint Centre research. x of them have defended their theses already.
  • post-doctoral researchers have been hosted by the Joint Centre.
  • The Joint Centre, which currently includes resident researchers, Ph.D. students, and post-docs, has funded person-years of Ph.D. students and person-years of post-docs. This support is helping to grow the talent pool available to the French research community.

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.