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
Formal specifications of programming languages
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-02-14 (09:00)
From: Jacques Garrigue <garrigue@m...>
Subject: Re: [Caml-list] Formal specifications of programming languages
From: Andrej Bauer <>
> 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