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.

Boolean Expression Simplifier
[19-Apr-2012, version
0.9.1.2,
Beta]

The Boolean Expression Simplifier library is an OCaml library providing means to simplify boolean expression.

Calcul avec OCaml
[25-Sep-2012, version
0.3]

These modules may be used as interactive calculus constructions when loaded in the ocaml pseudo_interpreter, or as calculus library.

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

A rewrite and constraint-solver tool.

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

A proof assistant.

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

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

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.

GeOCaml
[11-Feb-2003, version
0.1]

A tool allowing to handle easily euclidian geometry.

GlSurf
[25-Aug-2003, version
2.0,
Beta]

A program (similar to Surf) to draw surfaces from their implicit equations.

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

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

Hansei
[02-Jun-2009,
Development code]

HANSEI is the the embedded domain-specific language for probabilistic programming: for writing potentially infinite discrete-distribution models and performing exact inference, importance sampling and inference of inference.
HANSEI is an ordinary OCaml library, with probability distributions represented as ordinary OCaml programs. Delimited continuations let us reify non-deterministic programs as lazy search trees, which we may then traverse, explore, or sample. Thus an inference procedure and a model invoke each other as co-routines. Thanks to the delimited control, deterministic expressions look exactly like ordinary OCaml expressions, and are evaluated as such, without any overhead.
Inference procedures and probabilistic models are both ordinary OCaml functions. Both may be defined and extended by library users; both may appear in each other's code. Performing inference on a model that includes calls to inference procedures lets us parameterize distributions by distributions, and lets inference procedures measure their own accuracy. One application is modeling agents reasoning about each other's limited reasoning.

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.

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.

HSeq
[15-Jun-2006,
Alpha]

A simple tactical theorem prover for higher-order logic.

Interval computation library
[17-Apr-2012, version
1.2,
Stable]

This is an interval computation library for ocaml.

Link
[16-Sep-2002,
Alpha]

A theorem prover for Multiplicative Linear Logics based on PROOF NETS Construction.

mcmc-ocaml
[14-Apr-2011,
Development code]

A library for Markov-chain Monte Carlo
computations in OCaml.

Mesh
[14-Apr-2011, version
0.7,
Beta]

OCaml interface to various mesh generators, in particular triangle.

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.

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

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

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.

Mlgrace
[02-Nov-2004, version
0.1.0,
Beta]

A high-level interface to the Grace 2D plotting application. It makes extensive use of OCaml's labeled optional arguments, making the most common plotting operations quick and easy.

nlopt
[20-Jun-2012,
Development code]

OCaml bindings to the NLopt nonlinear optimization
library. The wrapper code implements an almost complete NLopt API (the
only exception are vector-valued constraints).

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.

OCaml-R
[11-Feb-2010, version
0.2,
Beta]

OCaml-R provides bindings to the R math library and the R library usable to embed R in your application.

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

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

OCamlmex
[02-May-2002]

An OCaml/Matlab interface.

Ocamlplot
[24-Nov-2003, version
0.5.6,
Beta]

An OCaml interface to the GNU libplot library.

Ocamlyices
[22-Sep-2010, version
0.4,
Beta]

Yet another binding for Yices SMT 1.x. Based on CamlIDL, this library
allows the access to both Yices APIs (full and light), unsatisfiable
cores, bit vectors, and more experimental features (interrupting,
switching between APIs).

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.

Ott
[08-Jan-2007, version
0.10.2,
Alpha]

tool for
semantic definitions of programming languages and calculi.
The tool takes as input a definition of a language syntax and semantic
relations, in a concise and readable ASCII notation that is close to
what one would write in informal mathematics. It builds parsers for
symbolic and concrete terms of the language, generates LaTeX to build
a typeset version of the definition, and generates Coq, HOL, and
Isabelle versions of the definition.

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.

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.

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.

sk
[21-Jan-2008,
Development code]

sk' is intended to allow experimentation with combinatory logic.

SPPoC
[21-Jun-2004, version
1.2.1,
Beta]

Symbolic Parameterized Polyhedral Calculator.

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.

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.