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] 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 (07:08)
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...>
Subject: Re: [Caml-list] ACL2 equivalent in Caml?

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

Jean-Christophe Filliātre (

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