一句话：提出作用域推断，将核心语言的作用域规则提升到表面语言，并证明脱糖保持 α-等价。
许多语言用语法糖将表面语言定义为更小核心语言的扩展，因此表面语言的作用域规则并不显式，而 IDE、重构工具等源码工具却依赖这些规则来展示信息并可靠操作。本文提出作用域推断，将定义在核心语言上的作用域规则提升到表面语言。作者引入一种新的绑定结构表示——将作用域视为预序（preorder），并给出理论进展：证明脱糖系统在仅为核心语言提供作用域规则的情况下仍保持 α-等价。论文还实现了所提出的系统。
Many languages use syntactic sugar to define parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules , are not immediately evident. Nevertheless, IDEs, refactorers, and other tools that traffic in source code depend on these rules to present information to users and to soundly perform their operations. In this paper, we show how to lift scoping rules defined on a core language to rules on the surface, a process of scope inference . In the process we introduce a new representation of binding structure---scope as a preorder---and present a theoretical advance: proving that a desugaring system preserves α-equivalence even though scoping rules have been provided only for the core language. We have also implemented the system presented in this paper.
@article{PombrioKW17,
title = {Inferring scope through syntactic sugar},
author = {Justin Pombrio and Shriram Krishnamurthi and Mitchell Wand},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110288}
}