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,See also the PPDP 2004 article on the semantics of reFLect by Sava Kristić and John Matthews.
‘A reflective functional language for hardware design and theorem proving’
Journal of Functional Programming, 16(2):157-196, March 2006.
The Forte 3 system includes an implementation of reFLect and has been made publicly available by Intel for noncommercial use. It can be obtained from a download page on Intel's website.
As a demonstrator of reFLect's reflection capabilities, I have written a small implementation of functional hardware description language (HDL) in reFLect:
\newcommand{\reFLect}{\textit{re\kern-0.07em F\kern-0.07emL\kern-0.29em\raisebox{0.56ex}{ect}}\xspace}