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

# The Caml Hump: Science :: Maths and Logic

## Older contribs

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.
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.
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).
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.
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.
Interval computation library [17-Apr-2012, version 1.2, Stable]
This is an interval computation library for ocaml.
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.
Author: Jeremy Bem.
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.
CiME [09-Jan-2012, version 3, Stable]
A rewrite and constraint-solver tool.
Author: Claude Marché.
Mesh [14-Apr-2011, version 0.7, Beta]
OCaml interface to various mesh generators, in particular triangle.
mcmc-ocaml [14-Apr-2011, Development code]
A library for Markov-chain Monte Carlo computations in OCaml.
Author: Will M. Farr.
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.
Coq [18-Oct-2010, version 8.3, Stable]
A proof assistant.
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).
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.
Gpr [30-Nov-2009, version 0.9.4, Beta]
A machine learning library for dealing with Gaussian process regression in OCaml.
Author: Markus Mottl.
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.
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.
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.
sk [21-Jan-2008, Development code]
sk' is intended to allow experimentation with combinatory logic.
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.
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.
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.
HSeq [15-Jun-2006, Alpha]
A simple tactical theorem prover for higher-order logic.
Author: Matthew Wahab.
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.
Author: John Harrison.
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.
DrGeocaml [29-Apr-2005, version 2004-05-07, Beta]
A dynamic geometry software using the Gtk toolkit. Large use of the DrawingArea widget.
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.
Author: Paul Pelzl.
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.
SPPoC [21-Jun-2004, version 1.2.1, Beta]
Symbolic Parameterized Polyhedral Calculator.
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.
ocamldelaunay [09-Feb-2004, version 1.1, Stable]
A simple-minded, O(N^2), floating-point, 2D Delaunay triangulator without constraints.
Author: Issac Trotts.
Ocamlplot [24-Nov-2003, version 0.5.6, Beta]
An OCaml interface to the GNU libplot library.
Author: Olivier Andrieu.
GlSurf [25-Aug-2003, version 2.0, Beta]
A program (similar to Surf) to draw surfaces from their implicit equations.
GeOCaml [11-Feb-2003, version 0.1]
A tool allowing to handle easily euclidian geometry.