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

The Caml Hump: Science :: Typing

Major applications
Coq [18-Oct-2010, version 8.3, Stable] Has a documentationHas a tutorial
A proof assistant.
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.
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.
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.
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.
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.