Personal tools
You are here: Home Events Abstract Archives 2007-2008 A Sound Semantics for OCaml light

A Sound Semantics for OCaml light

Scott Owens 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.

Document Actions