Our users' achievements

The initial version of this list has been collected by Basile Starynkevitch (Commissariat à l'Énergie Atomique, France).

• ASTREE is a static analyzer for C programs that proves the absence of run-time errors in critical embedded software. It has been applied to the flight control software of the Airbus 340 and 380 airplanes.
• SLAM, developed at Microsoft Research, is a static program analyzer that finds bugs in Windows device drivers.
• Lindows, a Linux distribution, uses several system management tools that were written in-house in OCaml. Here is a longer description.
• LexiFi develops financial analysis and pricing tools using MLFi, an extension of OCaml.
• Frank Dellaert's group at Georgia Tech have written several significant computer vision and robotics applications in Caml. Featured on CNN.
• The ALVE Recorder was written in Objective Caml. This program digitally records telephone calls. Contact Matt Boyd mattwb78756@yahoo.com for further information. (The dot-com crash of 2000 killed this product.)
• NBCi shopping used Objective Caml extensively, in the chain of tools developed by Liquid Market to gather and build the contents of the shopping engine, as well as in the transaction engine. (The dot-com crash of 2000 killed this product.)
• Unison, a file synchronization tool (e.g. between a notebook and a desktop PC), for Unix and Windows.
• FFTW. FFTW is a very fast C subroutine library for computing Discrete Fourier Transforms (DFT). It uses a powerful symbolic optimizer written in OCaml which, given a size N, generates highly optimized C code to compute DFTs of size N. FFTW received the 1999 Wilkinson prize for numerical software.
• Dwight VandenBerghe uses Ocaml in a financial system. He wrote: It's a financial simulation system for actuaries, used to determine the valuation of life insurance companies. I used Ocaml for the compiler portion of the system, and C++ for the runtime engine, which has to be very fast.
• GeneWeb, Genealogical database software with Web interface (Daniel de Rauglaudre, INRIA, France).
• Coq, theorem provers for reasoning on programs (INRIA, France).
• Odyssée, automatic differentiation of Fortran code (INRIA, France).
• Caravan automatic parallelisation and analysis of sequential and data parallel programs (Pierre Boulet, Univ. Lille 1 et Versailles, France).
• HOPS (program transformer, University of the Federal Armed Forces Munich, D-85577 Neubiberg, GERMANY).
• Ensemble is a toolkit for distributed processing ( Mark Hayden, université Cornell, Etats-Unis).
• sE - synchronousEifel, a tool for design and programming of embedded real-time reactive systems (Dr. Reinhard Budde, German National Research Center for Information Technology, ESPRIT projects SYRF et CRISYS, Germany).
• Switchware Active Networking projects (Michael Hicks, Univ. of Pennsylvania, Etats-Unis): Active networks explore the idea of allowing routing elements to be extensively programmed by the packets passing through them. This allows computation previously possible only at endpoints to be carried out within the network itself, thus enabling optimizations and extensions of current protocols as well as the development of fundamentally new protocols.
• Network filtering (Joshua D. Guttma n, Mitre Corporation, Boston, USA).
• Ocaml as a scripting langage Ching-Tsun Chou (Intel Corp, Californie, USA).
• Pict Pi-Calculus based exploratory languages (Univ. Pennsylvannie, USA).
• Network supervision Gilles FALCON France Telecom (division des réseaux nationaux).
• Bioinformatical software by Andrew Conway.
• Formal analysis of cryptographical protocols Stanford Research International, Computer Science Lab by David Monniaux.
• Hevea, A fast latex to html translator in Caml, (Luc Maranget).
• SPIKE. The SPIKE system is an automatic theorem prover for Horn equational logics. SPIKE has been developed in Nancy as part of the PROTHEO project (INRIA Lorraine and CRIN). Written in Caml Light, the program is provided with a graphic interface in TCL/TK that allows for interaction through the mouse and menus. SPIKE is designed for supporting the construction of correct specifications through verifying properties by induction.
• .... etc

This list is incomplete and we're still adding stuff to it.