Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

The Caml Hump: Science :: Maths and Logic

Scientific software
Bedwyr [06-Nov-2006, version 1.0, Stable] Has a documentation
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.
Native OCaml libraries
Boolean Expression Simplifier [19-Apr-2012, version, Beta]
The Boolean Expression Simplifier library is an OCaml library providing means to simplify boolean expression.
Native OCaml libraries
Calcul avec OCaml [25-Sep-2012, version 0.3] Has a documentation
These modules may be used as interactive calculus constructions when loaded in the ocaml pseudo_interpreter, or as calculus library.
Scientific software
CiME [09-Jan-2012, version 3, Stable] Has a documentation
A rewrite and constraint-solver tool.
Author: Claude Marché.
Major applications
Coq [18-Oct-2010, version 8.3, Stable] Has a documentationHas a tutorial
A proof assistant.
Scientific software
DrGeocaml [29-Apr-2005, version 2004-05-07, Beta] Has a documentation
A dynamic geometry software using the Gtk toolkit. Large use of the DrawingArea widget.
Development tools
Focalize [14-Jan-2013, version 0.8.0, Beta] Has a documentation
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.
Applications written in Caml
GlSurf [25-Aug-2003, version 2.0, Beta] Has a documentation
A program (similar to Surf) to draw surfaces from their implicit equations.
Scientific software
Gpr [30-Nov-2009, version 0.9.4, Beta] Has a documentation
A machine learning library for dealing with Gaussian process regression in OCaml.
Author: Markus Mottl.
Native OCaml libraries
Hansei [02-Jun-2009, Development code] Has a documentation
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.
Scientific software
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.
Author: Henri Binsztok.
Scientific software
HOL-light [22-May-2006, version 2.20, Stable] Has a documentationHas a tutorial
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.
Author: John Harrison.
Scientific software
HSeq [15-Jun-2006, Alpha]
A simple tactical theorem prover for higher-order logic.
Author: Matthew Wahab.
Native OCaml libraries
Interval computation library [17-Apr-2012, version 1.2, Stable] Has a documentation
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.
Native OCaml libraries
mcmc-ocaml [14-Apr-2011, Development code]
A library for Markov-chain Monte Carlo computations in OCaml.
Author: Will M. Farr.
Bindings with C libraries
Mesh [14-Apr-2011, version 0.7, Beta]
OCaml interface to various mesh generators, in particular triangle.
Scientific software
MetaPRL [16-Feb-2004] Has a documentationHas a tutorial
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.
Scientific software
Mjollnir [10-Jul-2009, version 2009-07-10, Beta]
Mjollnir implements various quantifier eliminations algorithms for the theory of real (or rational) linear arithmetic.
Author: David Monniaux.
Scientific software
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.
Native OCaml libraries
Mlgrace [02-Nov-2004, version 0.1.0, Beta] Has a tutorial
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.
Author: Paul Pelzl.
Bindings with C libraries
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).
Scientific software
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.
Author: David McClain.
Bindings with C libraries
OCaml-R [11-Feb-2010, version 0.2, Beta] Has a tutorial
OCaml-R provides bindings to the R math library and the R library usable to embed R in your application.
Scientific software
ocamldelaunay [09-Feb-2004, version 1.1, Stable]
A simple-minded, O(N^2), floating-point, 2D Delaunay triangulator without constraints.
Author: Issac Trotts.
Bindings with C libraries
OCamlmex [02-May-2002]
An OCaml/Matlab interface.
Author: Maurice Bremond.
Bindings with C libraries
Ocamlplot [24-Nov-2003, version 0.5.6, Beta]
An OCaml interface to the GNU libplot library.
Author: Olivier Andrieu.
Bindings with C libraries
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).
Scientific software
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.
Author: Paul Pelzl.
Applications written in Caml
Ott [08-Jan-2007, version 0.10.2, Alpha] Has a documentationHas a tutorial
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.
Scientific software
Phox [24-Apr-2002, version 0.83, Beta] Has a documentation
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.
Development tools
Pml [07-May-2007, Alpha] Has a documentation
PML will be a proof assistant based on a variant of the ML programming language which should also allow to write mathematics.
Scientific software
PsiLAB [02-Nov-2001, version 2.0, Stable] Has a documentation
Scientific and numerical research environment.
Author: Stefan Bosse.
Scientific software
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.
Toys - Examples
sk [21-Jan-2008, Development code]
sk' is intended to allow experimentation with combinatory logic.
Native OCaml libraries
SPPoC [21-Jun-2004, version 1.2.1, Beta]
Symbolic Parameterized Polyhedral Calculator.
Scientific software
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.
Author: Damien Doligez.
Scientific software
Zermelo Proof Checker [26-Jan-2012, version 1.0, Stable] Has a documentation
The Zermelo Proof Checker (ZPC) is a lightweight proof assistant based on standard set theory and Hindley-Milner type theory.
Author: Jeremy Bem.