A reflective functional language for hardware design and theorem proving

J. Grundy, T. Melham, and J. O'Leary, A reflective functional language for hardware design and theorem proving, Journal of Functional Programming, 16(2):157-196, March 2006.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself.

reFLect is apparently a follow-on to the earlier FL language (which I asked about in an earlier thread), the language used in Intel's Forte hardware verification environment. Within Forte, reFLect can be used to perform a seamless mix of theorem proving and model-checking (invocation of a model-checker is just a reFLect function call, with the source text of any call to the model-checker that returns true becoming a theorem of the logic). Tom Melham's reFLect page has a little more information, and also points out that a Linux version of the Forte system, including an implementation of reFLect, is freely downloadable from Intel.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


On the reFLect page I found a link to Lava, a similar project based on Haskell.
Does anyone know what are the « licensing issues » that it encountered and which forbid it's download ?

Actually, you can download

Actually, you can download it right from there.

But Lava is very hardware-oriented and not useful for high-level hardware simulation where Haskell would shine (and, actually, shines).

Don't know, but...

I don't what the licensing issues referred to on the Chalmers page are. But it appears that version 0.1a of Lava can be downloaded from here.