@techreport{RR-03-16,
  abstract = "This paper introduces&nbsp;<em>reFL<sup>ect</sup></em>, a functional programming language with reflection features intended for applications in hardware design and verification. The&nbsp;<em>reFL<sup>ect</sup></em>&nbsp;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&nbsp;<em>reFL<sup>ect</sup></em>&nbsp;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&nbsp;<em>reFL<sup>ect</sup></em>&nbsp;programs into the lambda-calculus using the same context mechanism.",
  author = "Jim Grundy and Tom Melham and John O'Leary",
  institution = "Oxford University Computing Laboratory",
  month = "October",
  number = "RR-03-16",
  title = "A Reflective Functional Language for Hardware Design and Theorem Proving",
  year = "2003",
}