X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fsites%2Finria.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fsites%2Finria.xml;h=0000000000000000000000000000000000000000;hp=ac3f5c23e4114963bfaa030b29e362df2e3eaecd;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/mowgli/home/xml/sites/inria.xml b/helm/mowgli/home/xml/sites/inria.xml deleted file mode 100644 index ac3f5c23e..000000000 --- a/helm/mowgli/home/xml/sites/inria.xml +++ /dev/null @@ -1,119 +0,0 @@ - - - - - - Institut National de Recherche en Informatique et Automatique (INRIA) - Rocquencourt - France - http://www.inria.fr -
Domaine de Voluceau, 78153 Rocquencourt Cedex, France
- - -

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.

- - - Lemme - http://www-sop.inria.fr/lemme - - - - - - - - -

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 - http://www.logical.inria.fr - - - -

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.

- - -