Version franšaiseWelcome 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.
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: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.
GNU Prolog -
Contact Web Administrator - Last modified: 2006/04/12