[Caml-list] ACL2 equivalent in Caml?

[Caml-list] ACL2 equivalent in Caml?

[Will Benton]

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?


thanks,
wb

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] ACL2 equivalent in Caml?

[Jean-Christophe Filliatre]

Will Benton writes:
 > 
 > 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?

There are  (at least) three  proof assistants written in  Caml, namely
Coq, HOL Light  and MetaPRL (URLs below). Caml  is their metalanguage,
that is you can write proof tactics in Caml for instance. But contrary
to ACL2  these are not  _directly_ programming languages on  which you
can  reason about. Yet  you can  use these  systems to  prove programs
correct. Coq for  instance (this is the one I  know) has an extraction
mechanism   which   automatically   generates   Caml   programs   from
constructive   proofs  of  their   specifications,  thus   correct  by
construction.

Regards,
-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)


http://coq.inria.fr/
http://www.cl.cam.ac.uk/users/jrh/hol-light/
http://cvs.metaprl.org:12000/metaprl/default.html

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] ACL2 equivalent in Caml?

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 954 bytes --]

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
---------------------------------------------

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]

[Caml-list] Re: ACL2 equivalent in Caml?

[Will Benton]

Thanks for all of the suggestions!  I'll check out these tools. 
(Christophe, I am interested in examining your PhoX-based solution, if
you can send me a pointer.)


best,
wb

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners