A Sound Semantics for OCaml light Export

@incollection{citeulike:2709522, 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.}, author = {Owens, Scott}, citeulike-article-id = {2709522}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-78739-6_1}, doi = {10.1007/978-3-540-78739-6_1}, journal = {Programming Languages and Systems}, keywords = {caml, formal-proof, hol, homepage, ott}, pages = {1--15}, posted-at = {2008-05-11 11:51:55}, priority = {3}, title = {A Sound Semantics for OCaml light}, url = {http://dx.doi.org/10.1007/978-3-540-78739-6_1}, year = {2008} }

TY - CHAP ID - citeulike:2709522 L3 - citeulike-article-id:2709522 N2 - 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. JF - Programming Languages and Systems EP - 15 TI - A Sound Semantics for OCaml light SP - 1 KW - caml KW - formal-proof KW - hol KW - homepage KW - ott AU - Owens, Scott PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-78739-6_1 ER -