A Theory of Name Resolution

In 2012 we introduced the NaBL name binding language, which supports high-level declarative specification of name binding and scope rules of (domain-specific) programming languages. In 2013 we introduced an incremental execution engine for NaBL, which recomputes only the resolution of those names that have been affected by a change. While this provides a powerful tool for language designers, we had a hard time explaining exactly how it worked. We kept getting the question ‘but what is the semantics of NaBL?’ and we didn’t have a good answer. Our attempts at formulating a high-level concise formalization of the semantics underlying the implementation proved that this was a non-trivial problem. In 2014 we finally managed to formulate a language-independent theory of name resolution in the form of a calculus that defines name resolution in a `scope graph’. The paper has been accepted for publication in the ESOP 2015 proceedings and is the ESOP nominee for the ETAPS 2015 best paper award:

A Theory of Name Resolution. Pierre Neron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. In Jan Vitek (editor), Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 2015

We have published an extended version of the paper as a technical report: A theory of name resolution with extended coverage and proofs (PDF)

Abstract: We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and language-independent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of alpha-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages.

Update April 15, 2015: The paper won the EAPLS 2015 Best Paper Award. ETAPS Daily