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. H^{E}V^{E}A: a fast LaTeX to HTML translator. ActiveDVI: a DVI previewer and graphic presenter for slides written in ^{L}A^{T}E^{X}. 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.

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