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 were tailored to support, among other things, the approach to formal verificiation embodied in Intel's Forte verification environment. The Forte approach 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.
Some further thoughts on the semantics of reflection in reFLect are in the following article:
Tom Melham, Raphael Cohn, and Ian Childs,
On the semantics of reFLect as a basis for a reflective theorem prover
arXiv Computing Research Repository, abs/1309.5742, September 2013.
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 wrote a small implementation of functional hardware description language (HDL) in reFLect:

This was 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}

Last updated Sun 17 Sep 2017 21:18:43 BST