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

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