Institut National de Recherche en Informatique et Automatique (INRIA) Rocquencourt

France

Domaine de Voluceau, 78153 Rocquencourt Cedex, France

Visit the institution home page.

Site responsible: Prof. Hugo Herbelin.

INRIA (National Institute for Research in Computer Science and Control) is a French public-sector scientific and technological institute operating under the dual authority of the Ministry of Research and the Ministry of Industry. INRIA's missions are ``to undertake basic and applied research, to design experimental systems, to ensure technology and knowledge transfer, to organise international scientific exchanges, to carry out scientific assessments, and to contribute to standardisation''.

The research carried out at INRIA brings together experts from the fields of computer science and applied mathematics covering the following areas: Networks and Systems; Software Engineering and Symbolic Computing; Man-Machine Interaction; Image Processing, Data Management, Knowledge Systems; Simulation and Optimisation of Complex Systems.

INRIA gathers in its premises around 2 100 persons including 1 600 scientists , many of which belong to partner organisations (CNRS, industrial labs, universities) and are assigned to work in common ``projects''. On INRIA's budget, around 500 full-time equivalent R&D positions can be accounted for.

A large number of INRIA senior researchers are involved in teaching and their PhD students (about 550) prepare their thesis within the different INRIA research projects (currently 74).

Its budget is roughly 90 MEuro, 20% of which comes from research and development contracts, royalties and sales. Industrial relations are strategic for INRIA:

Industrial contracts and European Projects.: Numerous industrial partners contract with the Institute for collaborative research. They are French or foreign companies, of all sizes. 400 such contracts are presently active. Roughly 40% of these contracts are European funded ones. Since 1984, 250 European Framework-Programme (FP) projects have been executed.
Technology companies.: As the ultimate step in technology transfer, researchers are party to the setting up of companies in order to implement their technology on the market. Thirty seven spin-off companies have been created since 1984. In 1999, INRIA has launched two subsidiaries to promote high-tech start-up companies: INRIA-TRANSFERT deals with early accompaniment of the future companies, whereas I-SOURCE GESTION provides for ``seed-money''.

INRIA is a member of ERCIM EEIG, European Research Consortium for Computer Science and Mathematics. Outside Europe, INRIA also has a significant activity: it has created joint research laboratories (Russia and China), signed cooperation agreements (NSF, India, Brazil, etc.) and promotes intensive scientific exchanges.

Projects developed by this site related to MOWGLI:

Lemme

Visit the project home page.

Members of the project also involved in MOWGLI:

The purpose of the Lemme project is to introduce and develop formal methods for use in writing scientific computing software. In scientific computing, algorithms and mathematics are at the forefront. We are thus developing tools and methods to help producing correct programs starting from the usual mathematical descriptions of data, algorithms, properties and proofs, structured into four research themes:

Proof environments (development of the Pcoq system in Java and its compatibility with XML/MathML).
Formalisation of mathematical theories (algebraic geometry, elementary algebra and analysis).
Certified implementation of scientific computing algorithms (computer algebra, arithmetics, logic).
Proofs on semantics of programming languages (Javacard).

The project belongs to the European working group Types, and to the French action AOC (Arithm\'etique des Ordinateurs Certifiée). It keeps up industrial collaborations with Dassault-Aviation (program proof environments), Alcatel Space Industry (certified numerical code), and GemPlus (Javacard certification), and also collaborates with teachers at university on the use of formal proofs and Web-based environments in mathematics courses.

LogiCal

Visit the project home page.

Members of the project also involved in MOWGLI:

The LogiCal team of INRIA is working on theoretical and practical aspects of mathematical proofs. It develops the Coq proof assistant, an implementation of an expressive formalism called Calculus of Inductive Constructions. Coq is used both for development of formal mathematics and for certification of programs, especially protocols and critical systems.

The LogiCal project is a joint project with University Paris 11. It is involved in the European TYPES working group and in several French actions. Especially, it is involved in the S-Java action aiming at certifying safety properties for JavaCard programs, in a project aiming at certifying algorithms used in computer algebra systems. LogiCal collaborates also on proof automation with France Telecom.

This page is hosted by the Department of Computer Science, University of Bologna.
Last updated Fri Feb 2 17:12:19 CET 2007.