Semantics of OCaml?

Is there a formal semantics of OCaml written down anywhere? Or anything close, e.g. formal semantics for a subset? I should probably know, but I don’t.

Don Sannella
University of Edinburgh

1 Like

There’s Scott Owens’ formal semantics for a subset, formalised in HOL: A Sound Semantics for OCaml light. I guess it was superseded by the semantics of CakeML, which is its own ML dialect, since Scott has worked on both.


I concur, Owen’s work on “OCaml light” is AFAIK the largest subset of OCaml that has been given formal, mechanised semantics.