Programming Research Group Research Report RR-03-16

A Reflective Functional Language for Hardware Design and Theorem Proving

Jim Grundy, Tom Melham and John O'Leary

October 2003, 39pp.

Abstract

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect 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 reFLect 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 reFLect programs into the lambda-calculus using the same context mechanism.


This paper is available as a 313,267 bytes pdf file.