Combining higher-order abstract syntax with first-order abstract syntax in ATS
K. Donnelly, Hongwei Xi · 2005
Abstract 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 ff-conversion, substitutionand 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 thatmakes use of a (restricted) form of dependent types. With this combination, we can readily define recursive functions over first-orderabstract 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