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.

翻译：Featherweight Generic Go (FGG) 是一个最小核心演算，用于建模编程语言 Go 的关键特性。它支持重载方法、接口类型、结构子类型和泛型。对 FGG 程序动态行为最直接的语义描述是基于接收者的运行时类型信息来解析方法调用。本文展示了一种不同的方法，通过定义从 FGG- 到无类型 λ-演算的面向类型翻译。FGG- 包含 FGG 的所有特性，但不包括类型断言。对 FGG- 程序的翻译将方法的可用性作为额外的字典参数提供证据，类似于 Haskell 类型类中已知的字典传递方法。然后，通过简单地在字典中查找方法定义即可解析方法调用。翻译结果中的每个程序与其源 FGG- 程序具有相同的动态语义。该结果的证明基于一个带步骤索引的语法逻辑关系。步骤索引确保了在存在递归接口类型和递归方法时关系的良基定义。尽管该翻译是非确定性的，它仍是自洽的。