English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

The Caml Hump: Applications written in Caml :: Scientific software


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.
Scientific software
CCured [26-May-2003, version 1.2.5, Stable] Has a documentation
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.
Scientific software
CIL [21-Aug-2002, version 1.3.7, Stable] Has a Godi packageHas a documentation
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.
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
FaCiLe [27-Sep-2004, version 1.1, Stable] Has a Godi packageHas a documentation
A library for constraint programming on finite domains.
Scientific software
Felix [17-Feb-2005, version 1.0.20, Stable] Has a documentationHas a tutorial
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.
Author: John Skaller.
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
Marionnet [08-Feb-2011, version 0.90.6, Stable] Has a documentation
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.
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.
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.
Scientific software
OCamlJitRun [13-Jul-2004, version 1.5, Stable] Has a documentation
A just in time translator of Ocaml bytecode into machine code (on x86, and perhaps sparcv9 & PowerPC in 32 bits mode).
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.
Scientific software
Oxford Oberon-2 Compiler [13-Sep-2002, version 2.0p5, Stable]
A portable compiler that translates Oberon-2 into bytecode.
Author: Mike Spivey.
Scientific software
PLAN [16-Sep-2002, version 3.22, Stable] Has a documentation
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.
Scientific software
Planets [30-Dec-2002, version 0.1.12, Stable]
A simple interactive program for playing with simulations of planetary systems.
Author: Yaron M. Minsky.
Scientific software
PoesiaMonIcap [19-Jun-2002, Stable] Has a documentation
An Internet Content Adaptation Protocol filter monitor (see www.i-cap.org).
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.
Scientific software
Securify [25-Sep-2003, Stable]
A tool to verify secrecy for cryptographic protocols.
Scientific software
Sumo [14-Apr-2003, Stable]
A system for extracting structural and possibly functional similarities in 3D structures of proteins.
Author: Martin Jambon.
Native OCaml libraries
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).
Scientific software
Why [29-Sep-2003, version 1.42, Stable] Has a documentation
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.
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.


Native OCaml libraries
CDuce [08-Jul-2004, version 0.2.0, Beta] Has a Godi packageHas a documentationHas a tutorial
A strongly typed higher-order functional programming language for XML documents with an efficient type-based runtime implementation.
Author: Alain Frisch.
Scientific software
Combinator Engine [26-Sep-2002, Beta]
A collection of the author's projects on combinator-based implementations of functional languages.
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.
Scientific software
EasyLanguage to C# translator [25-May-2007, Beta]
An EasyLanguage (http://lambda-the-ultimate.org/node/2201) to C# translator.
Author: Joël Reymond.
Scientific software
Fjavac [28-Dec-2005, version 0.4.1, Beta]
A functional Java 5 compiler.
Author: Stephen Tse.
Scientific software
Flow Caml [03-Jul-2003, version 1.03, Beta] Has a documentationHas a tutorial
A prototype implementation of an information flow analyzer for the Caml language.
Author: Vincent Simonet.
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.
Scientific software
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.
Author: Frama-C Development team (CEA LIST and INRIA Saclay).
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.
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
Logic File System [09-Jul-2008, version 0.5, Beta] Has a documentationHas a tutorial
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.
Author: Yoann Padioleau.
Scientific software
McCarthy [21-Feb-2006, Beta] Has a documentation
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.
Author: Geopoul.
Native OCaml libraries
Melt [24-Mar-2009, version 1.1.0, Beta] Has a documentation
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.
Author: Romain Bardou.
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
Mlpost [20-Apr-2010, version 0.8.0, Beta] Has a documentation
An Ocaml interface to MetaPost, a powerful software to draw pictures to be embedded in LaTeX documents.
Native OCaml libraries
MyCGR [03-Jul-2006, version 0.98, Beta] Has a tutorial
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.
Scientific software
NAB (Network in A Box) [14-Apr-2004, version 0.6, Beta] Has a documentationHas a tutorial
NAB is a network simulator targeted at wireless ad hoc and sensor networks.
Scientific software
nmag [22-Nov-2007, version 0.1beta, Beta] Has a documentation
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.
Scientific software
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.
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.
Scientific software
oc-FP [17-Nov-2003, Beta] Has a documentation
An OCAML implementation of John Backus' FP system.
Scientific software
oclisp [02-Apr-2008, version 0.5, Beta]
A minimal lisp interpreter, for educational purposes.
Author: Andrew Birkett.
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.
Scientific software
Phpsa [03-Apr-2006, version 0.1.1, Beta] Has a documentation
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.
Scientific software
Plasma [05-Mar-2012, version 0.6, Beta] Has a Godi packageHas a documentation
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.
Author: Gerd Stolpmann.
Scientific software
Schoca [26-Oct-2004, version 0.2.3, Beta] Has a Godi package
Schoca is an implementation of the Scheme language. The primary purpose of Schoca is the use as an embedded extension language in OCaml applications.
Author: Christoph Bauer.
Scientific software
SKS [12-Mar-2003, version 1.0.7, Beta] Has a documentation
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.
Author: Yaron M. Minsky.
Scientific software
Trx [28-Nov-2002, Beta] Has a documentation
Generic RPC transaction manager.
Author: Avik Chaudhuri.
Scientific software
XDuce [14-Mar-2003, version 0.4.0, Beta] Has a documentation
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.
Author: Haruo Hosoya.
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
AlphaProlog [30-Oct-2003, version 0.3, Alpha] Has a documentation
AlphaProlog is a logic programming language with built-in names, fresh name generation, name binding, and unification up to alpha-equivalence.
Author: James Cheney.
Scientific software
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.
Author: Kai Giese.
Scientific software
Dependent ML [18-Sep-2002, Alpha] Has a documentation
Dependent ML (DML) is an experimental extension of ML with a restricted form of dependent types.
Author: Hongwei Xi.
Scientific software
Dynamic Caml [16-May-2002, version 0.2, Alpha] Has a documentation
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.
Authors: Dmitry Lomov and Anton Moskal.
Scientific software
Fresh Objective Caml [03-Jul-2003, version 3.06-6, Alpha] Has a documentation
An extension of OCaml with facilities for correctly manipulating object-language syntax involving alpha-convertible names and binding operations.
Author: Mark Shinwell.
Scientific software
HSeq [15-Jun-2006, Alpha]
A simple tactical theorem prover for higher-order logic.
Author: Matthew Wahab.
Scientific software
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.
Scientific software
OCamIL [01-Jun-2004, Alpha]
OCamIL is an experimental OCAML compiler that targets Microsoft .NET.
Scientific papers
OCaml light [09-Nov-2007, Alpha] Has a documentation
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.
Scientific software
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).
Author: Jamie Clarkson.
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
virt-mem [18-Aug-2008, version 0.2.9, Alpha] Has a documentation
These are a collection of monitoring and management tools for virtual machines.

Development code

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

Scientific software
JoCaml [30-Aug-2012, version 4.00] Has a documentation
JoCaml is Objective Caml plus (&) the join calculus, that is, OCaml extended for concurrent and distributed programming.
Scientific software
MetaOCaml [28-Aug-2002, version 20020614]
A compiled, type-safe, multi-stage programming language.
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
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.
Author: Jason Hickey.
Scientific software
Polygen [14-Oct-2003, version 1.0pre] Has a documentation
PolyGen is a program for generating random sentences according to a grammar definition, that is following custom syntactical and lexical rules.
Author: Alvise Spano.