Combining Higher-Order Abstract Syntax with First-Order Abstract Syntax in ATS

MERLIN 2005

数学;计算机科学

Kevin Donnelly Hongwei Xi

Others  :  http://homepages.inf.ed.ac.uk/rpollack/TYPES/MERLIN_05/p58-donnelly.pdf
PID  :  52663

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Encodings based on higher-order abstract syntax represent the vari- ables of an object-language as the variables of a meta-language. Such encodings allow for the reuse of α-conversion, substitution and hypothetical judgments already defined in the meta-language and thus often lead to simple and natural formalization. However, it is also well-known that there are some inherent difficulties with higher-order abstract syntax in supporting recursive definitions. We demonstrate a novel approach to explicitly combining higher-order abstract syntax with first-order abstract syntax that makes use of a (restricted) form of dependent types. With this com- bination, we can readily define recursive functions over first-order abstract syntax while ensuring the correctness of these functions through higher-order abstract syntax. We present an implemen- tation of substitution and a verified evaluator for pure untyped call-by-value λ-calculus. Categories and Subject Descriptors D.3 [Software]: Program- ming Languages General Terms Languages, Verification