--- /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>???</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