Will Benton wrote:
> Hello,
> 
> I'm looking for an automated reasoning system like Moore's ACL2,
> except using the pure subset of Caml instead of pure Lisp.  Does such
> a tool exist?
> 
> 

I have a preliminary tool using PhoX for this (without modules, but with 
full pattern-matching). Mail me privately (or not privately) if you want 
more details.

It is based on the idea of Sylvain Baro's phd and he also has  an 
implementation. Mail Pascal Manoury (at Jussieu) for more info on his 
system.

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------