Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
@inproceedings{DonnellyXi05, author = {Kevin Donnelly and Hongwei Xi}, title = {Combining higher-order abstract syntax with first-order abstract syntax in {ATS}}, booktitle = {MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding}, year = {2005}, pages = {58--63}, location = {Tallinn, Estonia}, publisher = {ACM Press}, address = {New York, NY, USA}, abstrace = {{ Encodings based on higher-order abstract syntax represent the variables of an object-language as the variables of a meta-language. Such encodings allow for the reuse of $\alpha$-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 combination, 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 implementation of substitution and a verified evaluator for pure untyped call-by-value $\lambda$-calculus. }} }