Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 A Sound Semantics for OCaml light
OCaml light is a formal semantics for a substantial subset of the Objective Caml language. It is
written in Ott, and it
comprises a small-step operational semantics and a syntactic, non-algorithmic
type system. A type soundness theorem has been proved and mechanized using
the HOL-4 proof assistant, thereby
ensuring that the proof is free from errors. To ensure that the operational
semantics accurately models Objective Caml, an executable version of the
semantics has been created (and proved equivalent in HOL to the original,
relational version) and tested on a number of small test cases.
Note that while we have tried to make the semantics accurate, we are not part
of the OCaml development team - this is in no sense a normative specification
of the implemented language.
OCaml light supports the following Objective Caml features:
definitions
variant data types (e.g., type t = I of int | C of char),
record types (e.g., type t = {f : int; g : bool}),
parametric type constructors (e.g., type 'a t = C of 'a),
type abbreviations (e.g., type 'a t = 'a * int),
recursive and mutually recursive combinations of the above (excepting abbreviations),
exceptions,
values;
expressions for type annotations, sequencing, and primitive values (functions, lists, tuples, and records);
with (record update), if, while,
for, assert, try, and raise expressions;
let-based polymorphism (with an SML-style value restriction);
mutually-recursive function definitions via let rec;
pattern matching with nested patterns, as patterns, and "or" (|) patterns;
mutable references with ref, :=, and !;
polymorphic equality (the Objective Caml = operator);
31-bit word semantics for ints (using an existing HOL library);
IEEE-754 semantics for floats (using an existing HOL library).
OCaml light does not currently support objects, modules, pattern matching
guards (when), mutable records, or arrays.
Documents and Code
ESOP 2008 paper: A Sound Semantics for OCaml light.
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.
The Ott-generated proof assistant versions of the semantics for HOL, for Coq, and for
Isabelle/HOL (the latter two have not been validated by use in metatheoric proofs).