Re: [Caml-list] Formal specifications of programming languages

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>
> Christopher L Conway wrote:
> > But, Andrej, we don't even have an *informal* semantics. :-( You've
> > got to walk before you run.
> 
> Didn't Jacques say in a related post "Most of the type system is
> formalized, but there is no single place to look at"? Jacques, does the
> "type system" mean "type checking", "type inference", "operational
> semantics", or what. Heck, I should just look up the papers.

This is mostly about providing a formal type system (what you would
call type checking) and prove that it admits principal types (so that
an inference algorithm exists). Of course, for the modules system
there is no inference (it still use core-language inference).

Concerning the operational semantics, the reference manual is quite
complete I believe. Of course some things are left unspecified, but
this is actually part of the specification (you should be able to
write programs without knowing the exact evaluation orer for instance.)
 
> Maybe we should collect the relevant URLs and place them in the wiki. It
> would be a start. I might do that.

Good idea indeed.

Jacques Garrigue