Home

OCaml Light: A Formal Semantics For a Substantial Subset of the Objective Caml Language

OCaml Light: a formal semantics for a substantial subset of the Objective Caml language.

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.

From a team including Peter Sewell (Acute, HashCaml, Ott).

I continue to believe that things are heating up nicely in mechanized metatheory, which, in the multicore/multiprocessor world in which we now live, is extremely good news.

By Paul Snively at 2007-11-26 18:33 | Functional | General | Implementation | Object-Functional | Semantics | Theory | Type Theory | other blogs | 10357 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

due to Scott Owens

Thanks for that - but I should point out that this work is really due to Scott Owens. He's got a paper about it.

By Peter Sewell at Wed, 2007-11-28 17:27 | login or register to post comments

Hello, Peter!

Thanks for the reminder—it occurred to me that I hadn't given Scott or the rest of the team due credit when all I was trying to do was to relate OCaml Light to your other work, but I hadn't yet gotten around to correcting it myself. :-)

By Paul Snively at Wed, 2007-11-28 18:52 | login or register to post comments