+++ /dev/null
-<?xml version="1.0" encoding="iso-8859-1"?>
-
-<!DOCTYPE site SYSTEM "site.dtd">
-
-<site>
- <name>Institut National de Recherche en Informatique et Automatique (INRIA)
- Rocquencourt</name>
- <country>France</country>
- <url>http://www.inria.fr</url>
- <address>Domaine de Voluceau, 78153 Rocquencourt Cedex, France</address>
- <responsible file="inria/herbelin"/>
- <description>
- <p>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''.</p>
- <p>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.</p>
- <p>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.</p>
- <p>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).</p>
- <p>Its budget is roughly 90 MEuro, 20% of which comes from research and
- development contracts, royalties and sales. Industrial relations are
- strategic for INRIA:</p>
- <dl>
- <dt>Industrial contracts and European Projects.</dt>
- <dd>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.</dd>
-
- <dt>Technology companies.</dt>
- <dd>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''.</dd>
- </dl>
- <p>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.</p>
- </description>
- <project>
- <name>Lemme</name>
- <url>http://www-sop.inria.fr/lemme</url>
- <member file="inria/rideau"/>
- <member file="inria/naciri"/>
- <member file="inria/pottier"/>
- <member file="inria/bertot"/>
- <member file="inria/amerkad"/>
- <member file="inria/thery"/>
- <member file="inria/chicli"/>
- <description>
- <p>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:</p>
- <ul>
- <li>Proof environments (development of the Pcoq system in Java and its
- compatibility with XML/MathML).</li>
- <li>Formalisation of mathematical theories (algebraic geometry, elementary
- algebra and analysis).</li>
- <li>Certified implementation of scientific computing algorithms (computer
- algebra, arithmetics, logic).</li>
- <li>Proofs on semantics of programming languages (Javacard).</li>
- </ul>
- <p>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.</p>
- </description>
- </project>
- <project>
- <name>LogiCal</name>
- <url>http://www.logical.inria.fr</url>
- <member file="inria/herbelin"/>
- <member file="inria/delahaye"/>
- <description>
- <p>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.</p>
- <p>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.</p>
- </description>
- </project>
-</site>
projects / helm.git / blobdiff