Hello,

David McClain <David.McClain@Avisere.com> writes:

> I wonder, as a non-specialist in this area, how the goals of FPL squares
> with this result?

As a "real world" example, AMD is proving the FPU of its processors with
ACL2, which is a functional subset of Common Lisp. However, the FPU
themselves are not written in a functionnal language but in hardware
language translated in Register Transfer Language (RTL). A translator is
used for RTL->ACL2 translation and then proving.

  http://www.cs.utexas.edu/users/moore/acl2/


If I remember correctly, Coq has been used in Cristal research team to
prove part(?) of OCaml type system.

Yours,
david

PS: I'm neither a specialist in this area.
-- 
 David MENTRÉ <dmentre@linux-france.org>

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