The Caml Hump: Public Domain

An Objective Caml implementation of the continuation-passing-style output from Olivier Danvy's paper Functional Unparsing.

This is a toy implementation of Zope's TAL (Template Attribute Language) for OCaml, conveniently named 'Octal'. It is built on top of Camlp4 and Xml-Light. The purpose of TAL is to have a template that is a valid XML or HTML document that already renders like the resulting document.

A little tool for looking up entries from /etc/services.

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.

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.

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.

Simple design-by-contract support using camlp4.

A simple GUI for OCaml. It offers two kinds of widgets, to wit, buttons and an Emacs like mini-editor.The idea is to create a GUI with a very small footprint, that is easy to handle for final users, and productive for developers.