Software
Objective Caml
Objective Caml is our flagship implementation of the Caml language. From a language standpoint, it extends the core Caml language with a fully-fledged object and class layer, as well as a powerful module system, all joined together by a sound, polymorphic type system featuring type inference. The Objective Caml system is an industrial-strength implementation of this language, featuring a high-performance native-code compiler for several processor architectures (x86-32 bits, x86-64 bits, PowerPC, ARM, etc), as well as a bytecode compiler and interactive loop for quick development and portability. The Objective Caml distribution includes a standard library and a number of programming tools: replay debugger, lexer and parser generators, documentation generator, and the Camlp4 source pre-processor.
The CompCert C verified compiler
The Compcert verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC processor. The distinguishing feature of Compcert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to critical embedded programs.
Zenon
Zenon is an automatic theorem prover based on the tableaux method. Given a first-order statement as input, it outputs a fully formal proof in the form of a Coq proof script. It has special rules for efficient handling of equality and arbitrary transitive relations. Although still in the prototype stage, it already gives satisfying results on standard automatic-proving benchmarks. Zenon is designed to be easy to interface with front-end tools (for example integration in an interactive proof assistant), and also to be easily retargetted to output scripts for different frameworks (for example, Isabelle).
Alpha Caml
Cαml (pronounced "alpha-Caml") is an OCaml code generator that turns a so-called "binding specification" into safe and efficient implementations of the fundamental operations over terms that contain bound names. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding constructs: where are names bound in the data structure? what is the scope of such a binding? The automatically generated operations include substitution, computation of free names, and mechanisms to traverse and transform terms. This tool helps writers of interpreters, compilers, or other programs-that-manipulate-programs deal with α-conversion in a safe and concise style.
Menhir
Menhir is a new LR(1) parser generator for Objective Caml.
Menhir improves on its predecessor, ocamlyacc, in many ways:
more expressive language of grammars, including EBNF syntax and the
ability to parameterize a non-terminal by other symbols; support for
full LR(1) parsing, not just LALR(1); ability to explain conflicts in
terms of the grammar; etc.
WhizzyTeX
WhizzyTex is an Emacs minor mode for incremental viewing of LaTeX documents. The document is automatically processed and displayed while the user is editing it, in near-WYSIWYG manner.