University of Cambridge
4pm Tuesday 26th February 2008
Room 2511, JCMB, King's Buildings
OCaml light is a formal semantics for a substantial subset of Objective Caml's core 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. OCaml light's homepage is http://www.cl.cam.ac.uk/~so294/ocaml.
In this talk, I will present my OCaml light semantics and it's relationship to the Objective Caml language. I will furthermore discuss the role of mechanized proof, and also testing, in creating and validating the semantics.