The Caml Hump: Science :: Maths and Logic

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.

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

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

A rewrite and constraint-solver tool.

A proof assistant.

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

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.

A tool allowing to handle easily euclidian geometry.

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

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

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.

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 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.

A simple tactical theorem prover for higher-order logic.

This is an interval computation library for ocaml.

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

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

OCaml interface to various mesh generators, in particular triangle.

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 implements various quantifier eliminations algorithms for the theory of real (or rational) linear arithmetic.

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.

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.

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

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 provides bindings to the R math library and the R library usable to embed R in your application.

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

An OCaml/Matlab interface.

An OCaml interface to the GNU libplot library.

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 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.

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 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 will be a proof assistant based on a variant of the ML programming language which should also allow to write mathematics.

Scientific and numerical research environment.

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' is intended to allow experimentation with combinatory logic.

Symbolic Parameterized Polyhedral Calculator.

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.

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