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,Some further thoughts on the semantics of reflection in reFLect are in the following article:
‘A reflective functional language for hardware design and theorem proving’
Journal of Functional Programming, 16(2):157-196, March 2006.
Tom Melham, Raphael Cohn, and Ian Childs,See also the PPDP 2004 article on the semantics of reFLect by Sava Kristić and John Matthews.
‘On the semantics of reFLect as a basis for a reflective theorem prover’
arXiv Computing Research Repository, abs/1309.5742, September 2013.
As a demonstrator of reFLect's reflection capabilities, I wrote a small implementation of functional hardware description language (HDL) in reFLect: