OCaml light

by Scott Owens

(with Gilles Peskine, Peter Sewell, and Tom Ridge)

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.

Note that while we have tried to make the semantics accurate, we are not part of the OCaml development team - this is in no sense a normative specification of the implemented language.

OCaml light supports the following Objective Caml features:

OCaml light does not currently support objects, modules, pattern matching guards (when), mutable records, or arrays.

Documents and Code

History

Validate HTML 4.01 Strict