## Stable

Bedwyr
[06-Nov-2006, version
1.0,
Stable]

Bedwyr is an extended logic programming language that allows
model-checking directly on syntactic expressions possibly containing
bindings.
We believe that it's an interesting tool for computer scientists, as
it allows simple reasoning on declarative specifications, with several
good examples, notably bisimulation checking for the pi-calculus.
Other examples include type systems, games, logics, etc.

CCured
[26-May-2003, version
1.2.5,
Stable]

CCured is a source-to-source translator for C. It analyzes the C program to determine the smallest number of run-time checks that must be inserted in the program to prevent all memory safety violations.

CIL
[21-Aug-2002, version
1.3.7,
Stable]

CIL (C Intermediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs.

CiME
[09-Jan-2012, version
3,
Stable]

A rewrite and constraint-solver tool.

Coq
[18-Oct-2010, version
8.3,
Stable]

A proof assistant.

FaCiLe
[27-Sep-2004, version
1.1,
Stable]

A library for constraint programming on finite domains.

Felix
[17-Feb-2005, version
1.0.20,
Stable]

Felix is an Algol like strongly typed procedural programming language with a strong purely functional subsystem, including first class functions, pattern matching, variants, recursion, and (currently only) compile time parametric polymorphism.

HOL-light
[22-May-2006, version
2.20,
Stable]

HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness.

Marionnet
[08-Feb-2011, version
0.90.6,
Stable]

Marionnet is a virtual network laboratory: it allows users to define, configure and run complex computer networks without any need for physical setup. Only a single, possibly even non-networked GNU/Linux host machine is required to simulate a whole Ethernet network complete with computers, routers, hubs, switchs, cables, and more.
Support is also provided for integrating the virtual network with the physical host network.
As Marionnet is meant to be used also by inexperienced people, it features a very intuitive graphical user interface.

MLBrot
[15-Nov-2010, version
1.00,
Stable]

MLbrot is a program allowing to explore the Mandelbrot Set and produce
nice fractal images. With some extra work, can produce videos. Can be
helped by other computers, via internet, to speed up images calculations.

ocamldelaunay
[09-Feb-2004, version
1.1,
Stable]

A simple-minded, O(N^2), floating-point, 2D Delaunay triangulator
without constraints.

OCamlJitRun
[13-Jul-2004, version
1.5,
Stable]

A just in time translator of Ocaml bytecode into machine code (on x86, and perhaps sparcv9 & PowerPC in 32 bits mode).

Orpie
[03-Mar-2008, version
1.5.1,
Stable]

Orpie is a fullscreen RPN calculator for the console. Its operation is similar to that of modern HP calculators, but data entry has been optimized for efficiency on a PC keyboard. Features include extensive scientific calculator functionality, command completion, and a visible interactive stack.

Oxford Oberon-2 Compiler
[13-Sep-2002, version
2.0p5,
Stable]

A portable compiler that translates Oberon-2 into bytecode.

PLAN
[16-Sep-2002, version
3.22,
Stable]

PLAN is a resource-bounded functional programming language that uses a form of remote procedure call to realize active network packet programming. It is part of the SwitchWare Project.

Planets
[30-Dec-2002, version
0.1.12,
Stable]

A simple interactive program for playing with simulations of planetary systems.

PoesiaMonIcap
[19-Jun-2002,
Stable]

An Internet Content Adaptation Protocol filter monitor (see www.i-cap.org).

PsiLAB
[02-Nov-2001, version
2.0,
Stable]

Scientific and numerical research environment.

RegStab
[21-May-2012, version
2.0,
Stable]

RegSTAB is a SAT-solver able to deal with formula schemas:
you can give it a scheme of formulas such as "/\i=1..n
P_i -> P_i+1" (where n is a variable)
and it will be able to answer you if *all the formulas
of this form (i.e. for every value of n) are unsatisfiable*, i.e. it can treat at once an infinite set of
propositional formulas.

Securify
[25-Sep-2003,
Stable]

A tool to verify secrecy for cryptographic protocols.

Sumo
[14-Apr-2003,
Stable]

A system for extracting structural and possibly functional
similarities in 3D structures of proteins.

Timbuk
[05-Apr-2002, version
2.0,
Stable]

Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata).

Why
[29-Sep-2003, version
1.42,
Stable]

Why is a software verification tool.
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, HOL Light, Mizar and the decision procedures haRVey and Simplify.

Zermelo Proof Checker
[26-Jan-2012, version
1.0,
Stable]

The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and Hindley-Milner type theory.

## Beta

CDuce
[08-Jul-2004, version
0.2.0,
Beta]

A strongly typed higher-order functional programming language for XML documents with an efficient type-based runtime implementation.

Combinator Engine
[26-Sep-2002,
Beta]

A collection of the author's projects on combinator-based implementations of functional languages.

DrGeocaml
[29-Apr-2005, version
2004-05-07,
Beta]

A dynamic geometry software using the Gtk toolkit. Large use of the
DrawingArea widget.

EasyLanguage to C# translator
[25-May-2007,
Beta]

An EasyLanguage (http://lambda-the-ultimate.org/node/2201) to C# translator.

Fjavac
[28-Dec-2005, version
0.4.1,
Beta]

A functional Java 5 compiler.

Flow Caml
[03-Jul-2003, version
1.03,
Beta]

A prototype implementation of an information flow analyzer for the Caml language.

Focalize
[14-Jan-2013, version
0.8.0,
Beta]

FoCaLize is an integrated development environment to write high integrity
programs and systems. It provides a purely functional language to formally
express specifications, describe the design and code the algorithms. Within
the functional language, FoCaLize provides a logical framework to express the
properties of the code. A simple declarative language provides the natural
expression of proofs of those properties from within the program source code.

Frama-C
[25-Aug-2010, version
Boron-20100401,
Beta]

Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

Gpr
[30-Nov-2009, version
0.9.4,
Beta]

A machine learning library for dealing with Gaussian process regression in
OCaml.

HHMM library and designer
[16-Sep-2005, version
0.1.0,
Beta]

Hhl is a library for Hidden Markov Models (HMM) and Hierarchical HMMs (HHMMs) in Ocaml. Both are probabilistic sequence models. Hhd is a designer that allows to design by hand models and save them quickly.

Logic File System
[09-Jul-2008, version
0.5,
Beta]

LFS is a very expressive file system coded in OCaml.
LFS enables the user to access his files through an
additionnal mountpoint, /lfs, where powerful logic queries can be
issued and navigation can be done through different dimensions, like
date, size, or extension.

McCarthy
[21-Feb-2006,
Beta]

McCarthy is a simple, first-order functional programming language. The interpreter of this language is also called McCarthy. McCarthy is Turing-complete i.e. it can compute all Turing-computable functions on the integers. It is not suitable for general purpose programming as it offers only an elementary subset of the features found in general purpose programming languages, but it can serve as a model of computation.

Melt
[24-Mar-2009, version
1.1.0,
Beta]

Melt is a set of libraries and tools which allows you to program LaTeX
documents using OCaml. This combines the typesetting power of LaTeX with
the programming power of OCaml. It can be combined with Mlpost to
include figures.

Mjollnir
[10-Jul-2009, version
2009-07-10,
Beta]

Mjollnir implements various quantifier eliminations algorithms for the theory of real (or rational) linear arithmetic.

Mlpost
[20-Apr-2010, version
0.8.0,
Beta]

An Ocaml
interface to MetaPost, a powerful software to draw pictures to be
embedded in LaTeX documents.

MyCGR
[03-Jul-2006, version
0.98,
Beta]

This software implements the researches of the thesis of Peggy Cénac. Use the CGR to build a new family of tests of structure of sequences (i.i.d., markovian), empirically check the level and power of the tests and apply them on DNA sequences. Generalize the dinucleotide abundance profile to a CGR-based relative abundance profile and use this profile on DNA sequences to build taxonomy trees. Define CGR-trees, which are Digital Search Trees built from sequences, and check that the empirical longest branches, shortest branches and insertion level match the theorical results of the thesis.

NAB (Network in A Box)
[14-Apr-2004, version
0.6,
Beta]

NAB is a network simulator targeted at wireless ad hoc and sensor networks.

nmag
[22-Nov-2007, version
0.1beta,
Beta]

nmag is a micromagnetic simulation package based on the general purpose multi-physics library nsim. It is developed using Python and OCaml and interfaces both.

nML
[19-Sep-2002, version
0.92b,
Beta]

nML is a higher-order and typed programming language, and a dialect / harmony of Standard ML and Objective Caml. The nML compiler system drives the static analysis technologies to the limit, and it will embody the results of the LET project.

NML
[08-Jul-2004,
Beta]

a dynamically typed functional language whose syntax conforms closely to that of OCaml. In addition, it supports overloaded, vectorized, math operations, list comprehensions, and optional and keyword arguments in uncurried argument tuples, possibly with specified default values. It can access OLE compliant, and low-level COM interfaces, supports serial I/O and socket based communication, and provides an ADO connection to external databases. An Emacs mode is supported through a hacked Tuareg interface, as well as a Tcl/Tk interactive browser and interaction window with list pane access to a user modifiable documentation database.

oc-FP
[17-Nov-2003,
Beta]

An OCAML implementation of John Backus' FP system.

oclisp
[02-Apr-2008, version
0.5,
Beta]

A minimal lisp interpreter, for educational purposes.

Phox
[24-Apr-2002, version
0.83,
Beta]

PhoX is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version.

Phpsa
[03-Apr-2006, version
0.1.1,
Beta]

PHP string analyzer is a static program analyzer that approximates the string output of a PHP program with a context-free grammar. The analyzer can be used to check properties of a PHP program. For example, it can be used to validate dynamically generated Web pages by a PHP program.

Plasma
[05-Mar-2012, version
0.6,
Beta]

Map/Reduce and distributed filesystem.
This package contains two applications:
PlasmaFS is a distributed filesystem, Plasma MapReduce is a Map/Reduce framework on top of PlasmaFS.

Schoca
[26-Oct-2004, version
0.2.3,
Beta]

Schoca is an implementation of the Scheme language. The primary purpose of Schoca is the use as an embedded extension language in OCaml applications.

SKS
[12-Mar-2003, version
1.0.7,
Beta]

SKS is a new OpenPGP keyserver whose goal is to provide easy to deploy, decentralized, and highly reliable synchronization. That means that a key submitted to one SKS server will quickly be distributed to all key servers, and even wildly out-of-date servers, or servers that experience spotty connectivity, can fully synchronize with rest of the system.

Trx
[28-Nov-2002,
Beta]

Generic RPC transaction manager.

XDuce
[14-Mar-2003, version
0.4.0,
Beta]

XDuce ("transduce") is a typed programming language that is specifically designed for processing XML data. One can read an XML document as an XDuce value, extract information from it or convert it to another format, and write out the result value as an XML document. Since XDuce is statically typed, XDuce programs never yield run-time type errors and the resulting XML documents always conform specified types.

Zenon
[09-Jan-2012, version
0.6.3,
Beta]

Zenon is an automatic theorem prover written in OCaml.
Zenon handles first-order logic with equality. Its most important feature is
that it outputs the proofs of the theorems, in Coq-checkable form.

## Alpha

AlphaProlog
[30-Oct-2003, version
0.3,
Alpha]

AlphaProlog is a logic programming language with built-in names, fresh name generation, name binding, and unification up to alpha-equivalence.

Berto
[28-Feb-2011, version
0.1.1,
Alpha]

BERTO is an experimental ray tracer implemented in the Objective-Caml programming language. In this project
emphasis is put on physically based approximations and functional programming style.

Dependent ML
[18-Sep-2002,
Alpha]

Dependent ML (DML) is an experimental extension of ML with a restricted form of dependent types.

Dynamic Caml
[16-May-2002, version
0.2,
Alpha]

Dynamic Caml is a high-level run-time code generation library for Objective Caml.
Implementation is based on an abstract polymorphic type 'a code and function eval : 'a code -> 'a that evaluates it. We introduce various constructors for the code type. All types within dynamically generated code are statically checked at programs compile time.

Fresh Objective Caml
[03-Jul-2003, version
3.06-6,
Alpha]

An extension of OCaml with facilities for correctly manipulating object-language syntax involving alpha-convertible names and binding operations.

HSeq
[15-Jun-2006,
Alpha]

A simple tactical theorem prover for higher-order logic.

Mana
[23-May-2005, version
0.0.2,
Alpha]

Mana is a Japanese input engine, which converts phonetic
representation to proper written forms. Mana models Japanese language
as a HMM (Hidden Markovian Model), and its output is quite natural
even for a long sentence. In addition to Japanese, mana can be used
for Chinese once we have a necessary data.

OCamIL
[01-Jun-2004,
Alpha]

OCamIL is an experimental OCAML compiler that targets Microsoft .NET.

OCaml light
[09-Nov-2007,
Alpha]

OCaml light is a formal semantics for a substantial subset of the Objective Caml language. It is written in Ott, and it comprises a small-step operational semantics and a syntactic, non-algorithmic type system. A type soundness theorem has been proved and mechanized using the HOL-4 proof assistant, thereby ensuring that the proof is free from errors. To ensure that the operational semantics accurately models Objective Caml, an executable version of the semantics has been created (and proved equivalent in HOL to the original, relational version) and tested on a number of small test cases.

OPath
[16-Aug-2005, version
0.2,
Alpha]

OPath is a physically based renderer written in Objective-Caml, currently it
implements a variety of spectral BSDFs and several rendering algorithms
including distribution ray tracing, path tracing and 'Instant Global
Illumination'. It can render reasonably high polygon meshes and exclusively
uses area light sources (currently only spheres).

Pml
[07-May-2007,
Alpha]

PML will be a proof assistant based on a variant of the ML programming language which should also allow to write mathematics.

virt-mem
[18-Aug-2008, version
0.2.9,
Alpha]

These are a collection of monitoring and management tools for virtual machines.

## Development code

Texexpand
[29-Aug-2011,
Development code]

This project contains an OCaml re-implementation of some popular utilities like texexpand and delatex that were commonplace in the late 1990’s on all TeX/LaTeX user machines.

Xapi toolstack
[05-Nov-2009,
Development code]

The xapi toolstack, which provides the core Citrix Xenserver's functionalities, is a set of libraries and programs written in OCaml. It is approximately 200k lines of code developed from early 2006. Within Citrix, more than 40 people have already contributed to its source code.

## No status

JoCaml
[30-Aug-2012, version
4.00]

JoCaml is Objective Caml plus (&) the join calculus, that is, OCaml extended for concurrent and distributed programming.

MetaOCaml
[28-Aug-2002, version
20020614]

A compiled, type-safe, multi-stage programming language.

MetaPRL
[16-Feb-2004]

The MetaPRL system combines the properties of an interactive LCF-style tactic-based proof assistant, a logical framework, a logical programming environment, and a formal methods programming toolkit.

Mojave compiler
[20-May-2003, version
0.5.3]

A multi-language compiler supporting safe process migration and transactions for programs written in C, Caml, Java, and Pascal.

Polygen
[14-Oct-2003, version
1.0pre]

PolyGen is a program for generating random sentences according to a grammar definition, that is following custom syntactical and lexical rules.