Toward a general theory of names: binding and scope

High-level formalisms for reasoning about names and binding such uijn indices, various flavors of higher-order abstract syntax, ry of Contexts, and nominal abstract syntax address only one relatively restrictive form of scoping: namely, unary lexical scoping, in which the scope of a (single) bound name is a subtree bstract syntax tree (possibly with other subtrees removed due to shadowing). Many languages exhibit binding or renaming structure that does not fit this mold. Examples include binding transitions in the -calculus; unique identifiers in contexts, memory heaps, and XML documents; declaration scoping in modules and namespaces; anonymous identifiers in automata, type schemes, and Horn clauses; and pattern matching and mutual recursion constructs in functional languages. In these cases, it appears necessary r rearrange the abstract syntax so that lexical scoping can be used, or revert to first-order techniques. The purpose of this paper is to catalogue these "exotic" b...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: James Cheney
• Keywords: ICFP 2005, Lexical Scoping-based Syntax, Nominal Abstract Syntax, Programming Languages, Unary Lexical Scoping