On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover
Abstract
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 verification. ReFLect is similar to ML, but has a primitive data type whose elements are the abstract syntax trees of reFLect expressions themselves. Following the LCF paradigm, this is intended to serve as the object language of a higher-order logic theorem prover for specification and reasoning - but one in which object- and meta-languages are unified. The aim is to intermix program evaluation and logical deduction through reflection mechanisms. We identify some difficulties with the semantics of reFLect as currently defined, and propose a minimal modification of the type system that avoids these problems.
Keywords
Cite
@article{arxiv.1309.5742,
title = {On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover},
author = {Tom Melham and Raphael Cohn and Ian Childs},
journal= {arXiv preprint arXiv:1309.5742},
year = {2013}
}