On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover

Tom Melham, Raphael Cohn, Ian Childs

This paper explores the semantics of a combinatory fragment of reFLect, the lambda-calculus underlying a functional language used by Intel Corporation for hardware design and verif…