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
generative variant 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),
recursive and mutually recursive combinations of the above,
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, and arrays.
Documents and Code
Draft paper: A Sound Semantics for OCaml light.
Abstract. Few full-scale 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, for the first time, a large portion of the
semantics of Objective Caml, and 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).