Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: Caml-list Digest, Vol 32, Issue 43
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-02-13 (10:19)
From: Peter Sewell <Peter.Sewell@c...>
Subject: Re: Caml-list Digest, Vol 32, Issue 43

Jacques Garrigue <> wrote:
>Andrej Bauer <> 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:

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