A sound semantics for OCaml light

A sound semantics for OCaml light

[Scott Owens]

We are pleased to announce the public release of OCaml light, a  
formal semantics for a substantial, practical subset of the Objective  
Caml language. It is written in Ott, generating proof assistant  
definitions for HOL-4 and (in draft form) Coq and Isabelle/HOL. It  
comprises a small-step operational semantics and a syntactic, non- 
algorithmic type system. A type soundness theorem has been proved and  
mechanized using the HOL-4 proof assistant. To ensure that the  
operational semantics accurately models Objective Caml, an executable  
version of the semantics has been created (and proved equivalent in  
HOL to the original, relational version) and tested on a number of  
small test cases.

For more information please visit http://www.cl.cam.ac.uk/~so294/ocaml.

-Scott, Gilles, Peter, and Tom

Re: [Caml-list] A sound semantics for OCaml light

[Martin Jambon]

On Fri, 9 Nov 2007, Scott Owens wrote:

> We are pleased to announce the public release of OCaml light, a formal 
> semantics for a substantial, practical subset of the Objective Caml language.

May I suggest another name?
There's already Caml light.
In my opinion, having the name start with "ocaml" is a good idea (or 
should even be mandatory for every ocaml-derived product).
It should just be followed by something that is reasonably not ambiguous.



Martin

--
http://wink.com/profile/mjambon
http://martin.jambon.free.fr

Re: [Caml-list] A sound semantics for OCaml light

[Dario Teixeira]

> May I suggest another name?
> There's already Caml light.
> In my opinion, having the name start with "ocaml" is a good idea (or 
> should even be mandatory for every ocaml-derived product).
> It should just be followed by something that is reasonably not ambiguous.

Hi,

On a similar vein, has anyone noticed that "OCaml" and "O'Caml" produce
different results in Google?  Could some (naïve) language popularity
statistics be skewed unfavourably towards Ocaml because of this? And
should we as a community stick to one nomenclature to avoid this problem?...

Cheers,
Dario Teixeira



      ___________________________________________________________ 
Want ideas for reducing your carbon footprint? Visit Yahoo! For Good  http://uk.promotions.yahoo.com/forgood/environment.html

Re: [Caml-list] A sound semantics for OCaml light

[Christopher L Conway]

I think we as a community can agree that it is and always has been
OCaml, not O'Caml [1,2]. But that's not going to prevent a great
number of people from making the mistake. :-( I wonder if the folks at
INRIA gave any thought to the "Irish interpretation"? (I'm quite sure
the O'Haskell people did.)

Chris

[1] http://caml.inria.fr/resources/doc/faq/general.en.html#name-case
[2] http://en.wikipedia.org/wiki/Talk:Objective_Caml#.22Ocaml.22_to_.22O.27Caml_programming_language.22_move
[3] http://www.cs.chalmers.se/~nordland/ohaskell/

On Nov 9, 2007 9:46 AM, Dario Teixeira <darioteixeira@yahoo.com> wrote:
> > May I suggest another name?
> > There's already Caml light.
> > In my opinion, having the name start with "ocaml" is a good idea (or
> > should even be mandatory for every ocaml-derived product).
> > It should just be followed by something that is reasonably not ambiguous.
>
> Hi,
>
> On a similar vein, has anyone noticed that "OCaml" and "O'Caml" produce
> different results in Google?  Could some (naïve) language popularity
> statistics be skewed unfavourably towards Ocaml because of this? And
> should we as a community stick to one nomenclature to avoid this problem?...
>
> Cheers,
> Dario Teixeira
>
>
>
>       ___________________________________________________________
> Want ideas for reducing your carbon footprint? Visit Yahoo! For Good  http://uk.promotions.yahoo.com/forgood/environment.html
>
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

RE: [Caml-list] O'Caml vs OCaml (was: A sound semantics for OCaml light)

[David Allsopp]

> I think we as a community can agree that it is and always has been
> OCaml, not O'Caml [1,2]. But that's not going to prevent a great
> number of people from making the mistake. :-( I wonder if the folks at
> INRIA gave any thought to the "Irish interpretation"? (I'm quite sure
> the O'Haskell people did.)

With all due respect, but your first statement is refuted in your second
reference! I, as a very minimal example, would generally refer to it as
O'Caml, though occasionally mistype it (in a rush) - Gerd, for example, has
called it O'Caml today - though after your post his next one changed style!

The reference on the Inria site seems to clarify OCAML vs OCaml, not O'Caml
vs OCaml and if you grep recent list postings, you'll see a right old mix of
it: so possibly we don't agree!

Linguistically, it is acceptable for an acronym to become a word in its
right after long term adoption: for example, Laser (Light Amplification by
Stimulated Emission of Radiation), Sonar (SOund Navigation And Ranging),
Scuba (Self-Contained Underwater Breathing Apparatus) & Radar (RAdio
Detection And Ranging).

Hence CAML = Caml

For the sake of pedantry, the Irish spelling is in fact the more accurate
because O'Caml is the contraction of two words and the apostrophe should be
used to denote the missing letters in the contraction (cf. isn't, don't).

Hence Objective CAML = O'Caml

QED :o)

I fervently promise not air such pedantry on this list again...


David


> [1] http://caml.inria.fr/resources/doc/faq/general.en.html#name-case
> [2]
http://en.wikipedia.org/wiki/Talk:Objective_Caml#.22Ocaml.22_to_.22O.27Caml_
programming_language.22_move
> [3] http://www.cs.chalmers.se/~nordland/ohaskell/