Virtual building 8

Version franšaise

Welcome to ``virtual building 8'', a community of research groups at INRIA, Rocquencourt, France, with common interests in programming language design, semantics, implementation, proof systems, algorithms, and related topics.

Research groups:

Projet Gallium: the Caml programming language, type systems, compiler verification, program proof. (Formerly known as Projet Cristal.)

Projet Moscova: Mobility, Security, Concurrency, Verification and Analysis.

Projet Atoll: parsing & logic programming, computational linguistic, tabulation techniques, electronic documents.

Projet LogiCal: logic, calculus, formal proofs, the Coq proof assistant.

Projet Algo: analysis of algorithms, computer algebra and combinatorics.

Projet Contraintes: Constraint Programming (formerly projet Loco).

Software developments:

Caml: the Caml Light and Objective Caml compilers.

GNU Prolog: free native Prolog compiler with constraint solving over finite domains.

The Coq Proof Assistant.

Join calculus: a concurrent and distributed language.

clp(FD,S): a CLP system.

HEVEA: a fast LaTeX to HTML translator.

Active-DVI: a DVI previewer and graphic presenter for slides written in LATEX.

MMM: a Web browser with applets in Caml.


Publications available online (searchable index).

Technical reports and PhD theses (searchable index).

Other resources:

Home pages for our users.

Next events on our calendar.

Seminar announcements in the Paris area.

For visitors: directions to INRIA Rocquencourt.

The INRIA main Web site.

The INRIA Rocquencourt main Web site.

The anonymous FTP server.

Home - Cristal - Moscova - Atoll - LogiCal - Algo - Contraintes - Caml - Coq - Join - GNU Prolog - Homepages
Contact Web Administrator - Last modified: 2006/04/12