File created in October 1998.
Our users' achievements
The initial version of this list has been collected by
(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
(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 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.
Genealogical database software with Web interface (Daniel de Rauglaudre,
- Coq, theorem provers
for reasoning on programs (INRIA, France).
automatic differentiation of Fortran code (INRIA, France).
automatic parallelisation and analysis of sequential and data parallel
programs (Pierre Boulet,
Univ. Lille 1 et Versailles, France).
(program transformer, University of the Federal Armed Forces
Munich, D-85577 Neubiberg, GERMANY).
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).
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,
Pi-Calculus based exploratory languages (Univ. Pennsylvannie, USA).
- Network supervision Gilles FALCON France
Telecom (division des réseaux nationaux).
software by Andrew Conway.
- Formal analysis of cryptographical protocols Stanford Research International,
Computer Science Lab by David Monniaux.
A fast latex to html translator in Caml,
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.