论文标题
类型指导的，词典的词典翻译，对feather量级通用GO中的过载和结构性亚型的翻译
A Type-Directed, Dictionary-Passing Translation of Method Overloading and Structural Subtyping in Featherweight Generic Go
论文作者
论文摘要
轻量级通用GO（FGG）是一个最小的核心微积分，对编程语言GO的基本特征进行建模。它包括对超载方法，接口类型，结构性亚型和仿制药的支持。 FGG程序动态行为的最直接语义描述是基于接收器的运行时类型信息来解决方法调用。 本文通过定义从fgg-到未经类型的lambda-calculus的类型定向翻译来展示不同的方法。 FGG-包括FGG的所有功能，但类型断言。 FGG程序的翻译为其他字典参数提供了可用性的证据，类似于Haskell类型类已知的字典通话方法。然后，可以通过简单查找字典中的方法定义来解决方法调用。 翻译图像中的每个程序都具有与其源fgg-程序相同的动态语义。该结果的证明是基于句法，步骤索引的逻辑关系。在存在递归界面类型和递归方法的情况下，步骤索引确保了关系有充分的关系。尽管不确定性，但翻译是连贯的。
Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping and generics. The most straightforward semantic description of the dynamic behavior of FGG programs is to resolve method calls based on runtime type information of the receiver. This article shows a different approach by defining a type-directed translation from FGG- to an untyped lambda-calculus. FGG- includes all features of FGG but type assertions. The translation of an FGG- program provides evidence for the availability of methods as additional dictionary parameters, similar to the dictionary-passing approach known from Haskell type classes. Then, method calls can be resolved by a simple lookup of the method definition in the dictionary. Every program in the image of the translation has the same dynamic semantics as its source FGG- program. The proof of this result is based on a syntactic, step-indexed logical relation. The step-index ensures a well-founded definition of the relation in the presence of recursive interface types and recursive methods. Although being non-deterministic, the translation is coherent.
