论文标题
轻量轻量级的类型定向翻译方案的语义保存
Semantic preservation for a type directed translation scheme of Featherweight Go
论文作者
论文摘要
轻量级GO（FG）是一个最小的核心微积分，其中包含必需的GO功能，例如超载方法和接口类型。 FG程序动态行为的最直接语义描述是基于运行时类型信息解决方法调用。一种更有效的方法是应用一种类型定向的翻译方案，其中接口值被包含具体方法定义的字典代替。因此，可以通过简单查找字典中的方法定义来解决方法调用。确定通过类型定向的翻译方案获得的目标程序保留原始FG程序的语义是一项重要任务。为了建立此属性，我们采用逻辑关系，这些关系由类型索引以关联来源和目标程序。我们提供了严格的证据，并详细讨论了我们遇到的许多微妙的角落，包括由于递归界面和方法定义而需要阶跃索引的需求。
Featherweight Go (FG) is a minimal core calculus that includes essential Go features such as overloaded methods and interface types. The most straightforward semantic description of the dynamic behavior of FG programs is to resolve method calls based on run-time type information. A more efficient approach is to apply a type-directed translation scheme where interface-values are replaced by dictionaries that contain concrete method definitions. Thus, method calls can be resolved by a simple lookup of the method definition in the dictionary. Establishing that the target program obtained via the type-directed translation scheme preserves the semantics of the original FG program is an important task. To establish this property we employ logical relations that are indexed by types to relate source and target programs. We provide rigorous proofs and give a detailed discussion of the many subtle corners that we have encountered including the need for a step index due to recursive interfaces and method definitions.
