Skip to main content
Kent Academic Repository

A Sound Semantics for OCaml\(_{light}\)

Owens, Scott (2008) A Sound Semantics for OCaml\(_{light}\). In: Drossopoulou, Sophia, ed. Programming Languages and Systems 17th European Symposium on Programming. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 1-15. ISBN 978-3-540-78738-9. E-ISBN 978-3-540-78739-6. (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) (KAR id:31909)

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.
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: Book section
DOI/Identification number: 10.1007/978-3-540-78739-6_1
Uncontrolled keywords: test suite; operational semantic; symbolic execution; proof assistant; type constructor
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 10:23 UTC
Last Modified: 16 Nov 2021 10:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31909 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.