Computer Science – Logic in Computer Science
Scientific paper
2010-03-29
Computer Science
Logic in Computer Science
To appear in PPDP 2010
Scientific paper
Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda-conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha-Prolog, a nominal abstract syntax based logic programming language, to G-, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G-. This establishes G- as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.
No associations
LandOfFree
Relating Nominal and Higher-order Abstract Syntax Specifications does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Relating Nominal and Higher-order Abstract Syntax Specifications, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Relating Nominal and Higher-order Abstract Syntax Specifications will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-499415