]> matita.cs.unibo.it Git - helm.git/blob - helm/mowgli/home/xml/sites/inria.xml
New: two methods have been added to kill UWOBO and to start a new session
[helm.git] / 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>