Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Towards a General Theory of Names, Binding and Scope
Authors: James Cheney
Date:Sep 2005
Publication Title:Proc. MERLIN 2005
Publication Type:Conference Paper
High-level formalisms for reasoning about names and binding such as de Bruijn indices, various flavors of higher-order abstract syntax, the Theory 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 of the abstract 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 pi-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 to either 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 binding, renaming, and structural congruence situations; to argue that lexical scoping-based syntax techniques are sometimes either inappropriate or incapable of assisting in such situations; and to outline techniques for formalizing and proving properties of languages with more general forms of renaming and other structural congruences.
Links To Paper
Official version - ACM Portal
Bibtex format
author = { James Cheney },
title = {Towards a General Theory of Names, Binding and Scope},
book title = {Proc. MERLIN 2005},
year = 2005,
month = {Sep},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh