A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like programs, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantifiers, formal parameters, and blocks. It is a common observation that representing such binders using only first-order expressions is problematic since the notions of bound variable names, free and bound occurrences, equality up to alpha-conversion, substitution, etc., are not addressed naturally by the structure of first-order terms (labeled trees). This overview describes a higher-level and more declarative approach to representing syntax within such computational systems. In particular, we shall focus on a representation of syntax called higher-order abstract syntax and on a more primitive version of that representation called λ-tree syntax.
CITATION STYLE
Miller, D. (2000). Abstract syntax for variable binders: An overview. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 1861, pp. 239–253). Springer Verlag. https://doi.org/10.1007/3-540-44957-4_16
Mendeley helps you to discover research relevant for your work.