Version française
Home     About     Download     Resources     Contact us    

The Caml Hump: Science :: Typing

Stable

Major applications
Coq [18-Oct-2010, version 8.3, Stable] Has a documentationHas a tutorial
A proof assistant.

Beta

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.
Native OCaml libraries
pa_polymap [19-Oct-2007, Beta] Has a documentation
This is a tiny module combined with a camlp4 extension, which allows you to define polymorphic mappings, where the type of the data depends on the key.
Native OCaml libraries
Wallace [14-Mar-2003, version 2002/11/02, Beta]
Wallace is a generic subtyping-constraint-handling library. It deals with constraint solving and simplification, and it is parameterized by the definition of a type algebra. Its goal is to serve as a plug-in component in the design of a constraint-based type-checker, regardless of the programming language being analyzed.

Alpha

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.
Development tools
Saffire [31-May-2005, Alpha] Has a documentation
Saffire is a static analysis program that detects bugs in programs that use the OCaml/C foreign function interface. Saffire works by performing type inference across both OCaml and C to make sure that values are used consistently across the language boundary. For instance, if a OCaml passes a record to a C function, that C function should not treat the data as an integer. Saffire also tracks what C variables point into the OCaml heap and ensure they are always registered with CAMLparam/local before any allocation functions are called.
Author: Michael Furr.