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
[Caml-list] Dumping the OCaml state
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-08-31 (09:12)
From: Robert M. Solovay <solovay@M...>
Subject: Re: [Caml-list] Dumping the OCaml state

On Tue, 31 Aug 2004, Basile Starynkevitch [local] wrote:

> On Mon, Aug 30, 2004 at 11:57:05AM -0700, Robert M. Solovay wrote:
> >
> > I am using the HOL-light proof verifier which is written in OCaml.
> If you are talking about
> then it is written in CamlLight, not Ocaml. HOL-light does not seems
> to be actively developped (but I don't know really and may be wrong).
> CamlLight is somehow an ancestor of Ocaml, and it is not, as far as I
> know, actively worked upon. The Cristal team actively work on Ocaml
> and Caml Light is no more developped (but has gotten minor maintanance
> fixes sometimes)

	The version I have of HOL -light [obtained from Harrison in
private correspondence] is ported to OCaml.

	The interest of HOL-light [for me] is that it's what is currently
being used in the Flyspeck project of Tom Hales.

	--Bob Solovay
> Take everything above with a grain of salt. I don't know really
> HOL-light & Caml-light.
> --
> Basile STARYNKEVITCH -- basile dot starynkevitch at inria dot fr
> Project - temporarily
> --- all opinions are only mine
> -------------------
> To unsubscribe, mail Archives:
> Bug reports: FAQ:
> Beginner's list:

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: