English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] ACL2 equivalent in Caml?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-09-21 (13:34)
From: Christophe Raffalli <Christophe.Raffalli@u...>
Subject: Re: [Caml-list] ACL2 equivalent in Caml?
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 

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