A Reflective Functional Language for Hardware Design and Theorem Proving

Abstract

This paper introduces reFL^ect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFL^ect 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 reFL^ect language itself. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives and operational semantics based on a new use of contexts as expression constructors, and it presents a scheme for compiling reFL^ect programs into the lambda-calculus using the same context mechanism.