Skip to main content

A Sound Semantics for OCaml light

Owens, Scott (2008) A Sound Semantics for OCaml light. In: Drossopoulou, Sophia, ed. Programming Languages and Systems. Lecture Notes in Computer Science , 4960. pp. 1-15. Springer ISBN 978-3-540-78738-9. (doi:10.1007/978-3-540-78739-6_1) (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 currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/978-3-540-78739-6_1

Abstract

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)
DOI/Identification number: 10.1007/978-3-540-78739-6_1
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 10:23 UTC
Last Modified: 29 May 2019 09:39 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31909 (The current URI for this page, for reference purposes)
  • Depositors only (login required):