Demonstrating that information technology can prove mathematical conjectures. Improving interaction with scientific data. Contributing to progress in science and interdisciplinary research.
These are some of the critical challenges facing computer science and the natural sciences—and they are precisely the sorts of challenges being addressed by the Microsoft Research-INRIA Joint Centre, a joint effort recently inaugurated by the Insitut National de Recherche en Informatique et en Automatique (INRIA), the French national research institute for computer science, and Microsoft Research Cambridge.
The joint laboratory, located in Orsay, France, just outside Paris and formally inaugurated Jan. 11, is the product of an ongoing partnership between INRIA and Microsoft Research, which is celebrating its 15th year of innovation and which continues to pursue projects that set the stage for the future of computer science. The two organizations have been working together for the past few years to advance fundamental research in the software industry .
“Microsoft Research and INRIA have worked together informally for many years”, says Andrew Herbert, managing director of Microsoft Research Cambridge, “and now, with our joint laboratory, we can work more closely on topics of mutual interest, combining our respective strengths and talents.”
A staff of 15—expected to grow to 30 soon—is focusing on two key computer-research domains: formal methods, used to demonstrate long theorems or to validate communications protocols, and new forms of information interaction to provide a means to cope with the immense volume of data generated by modern scientific experiments.
As an example of the former, in 2004, Georges Gonthier, a senior researcher for Microsoft Research Cambridge, demonstrated his proof of the Four-Color Theorem, a conjecture that had first been offered in 1852. The theorem holds that for any map divided into regions, such as a political map of the world, its regions can be colored by using no more than four colors in a manner in which no adjacent regions receive the same color.
Gonthier and Benjamin Werner of INRIA are the team leaders of the joint lab’s Mathematic Components Project, which aims to prove that formal mathematical theories can be built from components, just like modern software. This work can be extended to improve significantly the actual and perceived quality of software.
A second project, led by Cédric Fournet, a researcher with Microsoft Research Cambridge, and INRIA’s James Leifer, plans to design formal tools for the simple programming of distributed calculations that include security guarantees. Their goal is to enable programmers, with reasonable effort, to express and prove correction properties, automatic or partly manual, as part of the program-development process.
A third, called Tools and Methodologies, is designed to provide formal specification and proofs and sets out to build a system capable of mechanically verifying the proof of systems specified in TLA+, a formal, high-level language used to specify algorithms and systems. This effort is being led by INRIA’s Damien Doligez and Stephan Merz, along with Leslie Lamport, a principal researcher from Microsoft Research Silicon Valley.
In addition, Wendy MacKay of INRIA and Mary Czerwinski, research-area manager of the Human-Centered Computing groups within Microsoft Research Redmond, are working on the Re-Activity project, one of a number of areas of investigation into IT tools for science.
The Microsoft-INRIA joint effort began on April 26, 2005, when Steve Ballmer, Microsoft chief executive officer, signed a memorandum of agreement with François d’Aubert, the French minister for research, and Gilles Kahn, chairman of INRIA, to announce the creation of a joint laboratory in France. On Oct. 24 of that year, Bill Gates, Microsoft chairman, signed a framework agreement with François Goulard, French minister for research, and Kahn, and a laboratory, hosted by the INRIA Futurs research unit, was established at Orsay Université.
The centre, directed by Jean-Jacques Lévy, INRIA research director, is governed by a management committee consisting of equal numbers of representatives from Microsoft and INRIA. Researchers at the lab work openly and collaboratively, and the results of their work will be published in scientific publications and will be distributed through the creation of software tools and prototypes that will be made publically available to the scientific community. Microsoft and INRIA will jointly determine the commercial application of research performed at the laboratory.