Semantics of the reFLect Language

reFLect is a new functional language, developed at Intel for use in hardware design and verification. It contains features intended to facilitate the construction, analysis, and manipulation of the language’s own programs. It is also intended to be the executable subset of the term language of a theorem prover based on higher order logic. In this paper, we consider core reFLect —a language that extends a polymorphically typed λ-calculus with a datatype for programs and with constructs for splicing programs into programs and for defining functions that inspect and modify programs. We prove that the reduction semantics for this language is strongly normalizing and confluent. We also give a set-theoretical denotational semantics for the language and prove that the reduction semantics is sound with respect to the denotational semantics. These results provide the basis for developing the semantics of reFLect’s extension of higher order logic and proving its soundness