On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover
On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover
复制标题
论作为反射定理证明者基础的 ReFLect 语义
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Ian Childs
中科院分区：
文献类型：
--
作者：
T. Melham;Raphael Cohn;Ian Childs
本文探讨了一个组合片段的reFLect，底层的函数式语言，英特尔公司用于硬件设计和验证的微积分的语义。ReFLect类似于ML，但具有基本数据类型，其元素是reFLect表达式本身的抽象语法树。遵循LCF范式，它旨在作为高阶逻辑定理证明器的对象语言，用于规范和推理-但其中对象语言和元语言是统一的。其目的是通过反射机制混合程序评估和逻辑推理。我们确定了一些困难与目前定义的reFLect的语义，并提出了一个最小的修改类型系统，以避免这些问题。
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.