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] Formal Methods
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-09-30 (17:54)
From: David MENTRE <dmentre@l...>
Subject: [Off-topic] Re: [Caml-list] Formal Methods

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.


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


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