A Sound Semantics for OCaml light

Owens, Scott (2008) A Sound Semantics for OCaml light. In: 17th European Symposium on Programming, ESOP 2008, March 29th - April 6th, 2008, Budapest, Hungary. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


Few programming languages have a mathematically rigorous definition or metatheory—in part because they are perceived as too large and complex to work with. This paper demonstrates the feasibility of such undertakings: we formalize a substantial portion of the semantics of Objective Caml’s core language (which had not previously been given a formal semantics), and we develop a mechanized type soundness proof in HOL. We also develop an executable version of the operational semantics, verify that it coincides with our semantic definition, and use it to test conformance between the semantics and the OCaml implementation. We intend our semantics to be a suitable substrate for the verification of OCaml programs.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 10:23
Last Modified: 18 Mar 2013 14:37
Resource URI: https://kar.kent.ac.uk/id/eprint/31909 (The current URI for this page, for reference purposes)
  • Depositors only (login required):