Re: Caml-list Digest, Vol 32, Issue 43

[Peter Sewell <Peter.Sewell@cl.cam.ac.uk>]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
>Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si> wrote:
>> Out of curiosity, is there a document describing the current ocaml
>> typing system, other than the compiler source code?
>>
>> More generally, what level of formal specification and verification does
>> ocaml reach? None, well commented code, a fragment of the language is
>> formalized, someone's PhD described the compiler, there is an official
>> document describing the compiler, God gave Xavier the type system on Mt
>> Blanc, or what?
>
>Most of the type system is formalized, but there is no single place to
>look at.  Caml Special Light (ocaml minus objects and variants) was
>mostly based on Xavier's work, so you can look at at his papers for that part 

Also for that part of the language, Scott Owens has a type system and
operational semantics, with a formalised soundness proof:

  http://www.cl.cam.ac.uk/~so294/ocaml/

It's not a normative specification, but does aim to be rather close to the
behaviour of the implementation.

Peter