helm/mowgli/home/xml/sites/inria.xml

   1 <?xml version="1.0" encoding="iso-8859-1"?>
   2
   3 <!DOCTYPE site SYSTEM "site.dtd">
   4
   5 <site>
   6  <name>Institut National de Recherche en Informatique et Automatique (INRIA)
   7    Rocquencourt</name>
   8  <country>France</country>
   9  <url>http://www.inria.fr</url>
  10  <address>Domaine de Voluceau, 78153 Rocquencourt Cedex, France</address>
  11  <responsible file="inria/herbelin"/>
  12  <description>
  13   <p>INRIA (National Institute for Research in Computer Science and
  14      Control) is a French public-sector scientific and technological
  15      institute operating under the dual authority of the Ministry of
  16      Research and the Ministry of Industry. INRIA's missions are ``to
  17      undertake basic and applied research, to design experimental systems,
  18      to ensure technology and knowledge transfer, to organise international
  19      scientific exchanges, to carry out scientific assessments, and to
  20      contribute to standardisation''.</p>
  21   <p>The research carried out at INRIA brings together experts from the
  22      fields of computer science and applied mathematics covering the
  23      following areas: Networks and Systems; Software Engineering and
  24      Symbolic Computing; Man-Machine Interaction; Image Processing, Data
  25      Management, Knowledge Systems; Simulation and Optimisation of Complex
  26      Systems.</p>
  27   <p>INRIA gathers in its premises around 2 100 persons including 1 600
  28      scientists , many of which belong to partner organisations (CNRS,
  29      industrial labs, universities) and are assigned to work in common
  30      ``projects''. On INRIA's budget, around 500 full-time equivalent R&amp;D
  31      positions can be accounted for.</p>
  32   <p>A large number of INRIA senior researchers are involved in teaching
  33      and their PhD students (about 550) prepare their thesis within the
  34      different INRIA research projects (currently 74).</p>
  35   <p>Its budget is roughly 90 MEuro, 20% of which comes from research and
  36      development contracts, royalties and sales. Industrial relations are
  37      strategic for INRIA:</p>
  38   <dl>
  39    <dt>Industrial contracts and European Projects.</dt>
  40    <dd>Numerous industrial partners contract with the Institute for
  41        collaborative research. They are French or foreign
  42        companies, of all sizes. 400 such contracts are presently
  43        active. Roughly 40% of these contracts are European funded
  44        ones. Since 1984, 250 European Framework-Programme (FP)
  45        projects have been executed.</dd>
  46
  47    <dt>Technology companies.</dt>
  48    <dd>As the ultimate step in technology transfer, researchers are party to
  49        the setting up of companies in order to implement their
  50        technology on the market. Thirty seven spin-off companies
  51        have been created since 1984. In 1999, INRIA has launched
  52        two subsidiaries to promote high-tech start-up companies:
  53        INRIA-TRANSFERT deals with early accompaniment of the
  54        future companies, whereas I-SOURCE GESTION provides for
  55        ``seed-money''.</dd>
  56   </dl>
  57   <p>INRIA is a member of ERCIM EEIG, European Research Consortium for
  58      Computer Science and Mathematics. Outside Europe, INRIA also has a
  59      significant activity: it has created joint research laboratories
  60      (Russia and China), signed cooperation agreements (NSF, India, Brazil,
  61      etc.) and promotes intensive scientific exchanges.</p>
  62  </description>
  63  <project>
  64   <name>Lemme</name>
  65   <url>http://www-sop.inria.fr/lemme</url>
  66   <member file="inria/rideau"/>
  67   <member file="inria/naciri"/>
  68   <member file="inria/pottier"/>
  69   <member file="inria/bertot"/>
  70   <member file="inria/amerkad"/>
  71   <member file="inria/thery"/>
  72   <member file="inria/chicli"/>
  73   <description>
  74    <p>The purpose of the Lemme project is to introduce and develop formal
  75       methods for use in writing scientific computing software. In scientific
  76       computing, algorithms and mathematics are at the forefront. We are thus
  77       developing tools and methods to help producing correct programs starting
  78       from the usual mathematical descriptions of data, algorithms, properties
  79       and proofs, structured into four research themes:</p>
  80    <ul>
  81     <li>Proof environments (development of the Pcoq system in Java and its
  82         compatibility with XML/MathML).</li>
  83     <li>Formalisation of mathematical theories (algebraic geometry, elementary
  84         algebra and analysis).</li>
  85     <li>Certified implementation of scientific computing algorithms (computer
  86         algebra, arithmetics, logic).</li>
  87     <li>Proofs on semantics of programming languages (Javacard).</li>
  88    </ul>
  89    <p>The project belongs to the European working group Types, and to the
  90       French action AOC (Arithm\'etique des Ordinateurs Certifiée). It keeps
  91       up industrial collaborations with Dassault-Aviation (program proof
  92       environments), Alcatel Space Industry (certified numerical code), and
  93       GemPlus (Javacard certification), and also collaborates with teachers at
  94       university on the use of formal proofs and Web-based environments in
  95       mathematics courses.</p>
  96   </description>
  97  </project>
  98  <project>
  99   <name>LogiCal</name>
 100   <url>http://www.logical.inria.fr</url>
 101   <member file="inria/herbelin"/>
 102   <member file="inria/delahaye"/>
 103   <description>
 104    <p>The LogiCal team of INRIA is working on theoretical and practical
 105       aspects of mathematical proofs. It develops the Coq proof assistant,
 106       an implementation of an expressive formalism called Calculus of
 107       Inductive Constructions. Coq is used both for development of formal
 108       mathematics and for certification of programs, especially protocols
 109       and critical systems.</p>
 110    <p>The LogiCal project is a joint project with University Paris 11.  It
 111       is involved in the European TYPES working group and in several French
 112       actions. Especially, it is involved in the S-Java action aiming at
 113       certifying safety properties for JavaCard programs, in a project
 114       aiming at certifying algorithms used in computer algebra
 115       systems. LogiCal collaborates also on proof automation with France
 116       Telecom.</p>
 117   </description>
 118  </project>
 119 </site>