TY - GEN
T1 - Abstract syntax for variable binders
T2 - 1st International Conference on Computational Logic, CL 2000
AU - Miller, Dale
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000/1/1
Y1 - 2000/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84867771131
U2 - 10.1007/3-540-44957-4_16
DO - 10.1007/3-540-44957-4_16
M3 - Conference contribution
AN - SCOPUS:84867771131
T3 - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
SP - 239
EP - 253
BT - Computational Logic - CL 2000 - 1st International Conference, Proceedings
A2 - Lloyd, John
A2 - Dahl, Veronica
A2 - Furbach, Ulrich
A2 - Kerber, Manfred
A2 - Lau, Kung-Kiu
A2 - Palamidessi, Catuscia
A2 - Pereira, Luís Moniz
A2 - Sagiv, Yehoshua
A2 - Stuckey, Peter J.
PB - Springer Verlag
Y2 - 24 July 2000 through 28 July 2000
ER -