Semantics of the reFLect Language
Sava Krstic and John Matthews
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 lambda-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.