ReFLect 语义作为反射式定理证明器基础的研究
计算机科学中的逻辑
2013-09-24 v1
摘要
本文探讨了 reFLect 的组合子片段的语义，reFLect 是英特尔公司用于硬件设计与验证的功能性语言所基于的 lambda 演算。ReFLect 类似于 ML，但拥有一种原始数据类型，其元素即为 reFLect 表达式本身的抽象语法树。遵循 LCF 范式，这旨在作为高阶逻辑定理证明器的对象语言，用于规范说明与推理，但该证明器统一了对象语言与元语言。其目标是通过反射机制交织程序求值与逻辑演绎。我们指出了当前 reFLect 语义定义中存在的一些困难，并提出了一种类型系统的最小化修改以规避这些问题。
引用
@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}
}