[TYPES/announce] A sound semantics for OCaml light

[Scott Owens]

We are pleased to announce the public release of OCaml light, a  
formal semantics for a substantial, practical subset of the Objective  
Caml language. It is written in Ott, generating proof assistant  
definitions for HOL-4 and (in draft form) Coq and Isabelle/HOL. 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. 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.

For more information please visit http://www.cl.cam.ac.uk/~so294/ocaml.

-Scott, Gilles, Peter, and Tom