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

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

The Caml Hump: OCaml light

OCaml light

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.
Homepage ]
Author:Peter Sewell, Tom Ridge, Gilles Peskine, and Scott Owens.
Last modification date:09-Nov-2007
Development status:Alpha
Kind: Documentations :: Scientific papers
Applications written in Caml :: Scientific software
Topic: Science :: Typing