Strong Normalization for System F by HOAS on Top of FOAS
Strong Normalization for System F by HOAS on Top of FOAS
复制标题
基于 FOAS 的 HOAS 对系统 F 的强标准化
DOI：
10.1109/lics.2010.48
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Christopher J. Osborn
中科院分区：
文献类型：
--
作者：
A. Popescu;Elsa L. Gunter;Christopher J. Osborn
我们提出了一个关于HOAS(高阶抽象语法)的观点，并沿着这一观点在HOAS中进行了广泛的练习。本文的观点是，HOAS可以被合理而有效地视为FOAS(一阶抽象语法)之上的定义扩展。因此，HOAS不仅是一种编码技术，而且是一阶现实的更高阶视图。在标准的数学宇宙中发展了丰富的概念和证明原理的集合，以赋予这一观点技术生命。这个练习包括系统F的强正规化的一个新证明。这里给出的概念和结果已经在定理证明器Isabelle/HOL中形式化。
We present a point of view concerning HOAS(Higher-Order Abstract Syntax) and an extensive exercise in HOAS along this point of view. The point of view is that HOAS can be soundly and fruitfully regarded as a definitional extension on top of FOAS (First-Order Abstract Syntax). As such, HOAS is not only an encoding technique, but also a higher-order view of a first-order reality. A rich collection of concepts and proof principles is developed inside the standard mathematical universe to give technical life to this point of view. The exercise consists of a new proof of Strong Normalization for System F. The concepts and results presented here have been formalized in the theorem prover Isabelle/HOL.