* Re: Caml-list Digest, Vol 32, Issue 43
[not found] <20080213100127.24366BC73@yquem.inria.fr>
@ 2008-02-13 10:19 ` Peter Sewell
0 siblings, 0 replies; only message in thread
From: Peter Sewell @ 2008-02-13 10:19 UTC (permalink / raw)
To: caml-list; +Cc: Peter.Sewell
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
^ permalink raw reply [flat|nested] only message in thread