The reFLect Programming Language

reFLect is a functional programming language designed and implemented by a team at Intel Corporation's Strategic CAD Labs under the direction of Jim Grundy. The language is strongly typed and similar to ML, but provides certain reflection features intended for applications in industrial hardware design and verification. Like LISP, reFLect has quotation and antiquotation constructs that may be used to construct and decompose expressions in the language itself. Unlike LISP, these mechanisms are typed. The language also provides a primitive mechanism for pattern-matching, and in particular for defining functions over code by pattern-matching on the structure of reFLect expressions.

These features are tailored to support, among other things, the approach to formal verificiation embodied in Intel's Forte verification environment. Forte combines several model checking and decision algorithms with lightweight theorem proving in higher-order logic. These reasoning tools are tightly integrated within reFLect, allowing the environment to be flexibly customised and large proof efforts to be organized and scripted effectively.

The following paper, in the Journal of Functional Programming, gives a detailed account of the design of the reFLect language and its semantics:

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.
See also the PPDP 2004 article on the semantics of reFLect by Sava Kristić and John Matthews.


As a demonstrator of reFLect's reflection capabilities, I have written a small implementation of functional hardware description language (HDL) in reFLect:

This is inspired by Lava, a hardware description language built on the Haskell functional programming language. Lava supports circuit netlist generation as well as simulation (execution) from a single Haskell source. My implementation shows how you can use some of the reflection features of reFLect to achieve this in a rather elegant way.

LaTeX Macro for Typesetting ‘reFLect’

\newcommand{\reFLect}{\textit{re\kern-0.07em F\kern-0.07emL\kern-0.29em\raisebox{0.56ex}{ect}}\xspace}

Tom Melham, last updated in July 2006.