一句话：提出将 FGG− 类型指导翻译为无类型 lambda 演算，用字典传递实现方法调用解析，并证明语义保持与一致性。
Featherweight Generic Go（FGG）是刻画 Go 核心特性（重载方法、接口类型、结构化子类型与泛型）的极简演算。通常其动态行为依赖接收者运行时类型信息来解析方法调用。本文提出另一种途径：定义从 FGG−（FGG 去掉类型断言）到无类型 lambda 演算的类型指导翻译。该翻译把方法可用性作为额外字典参数传递，类似 Haskell 类型类的字典传递；方法调用只需在字典中查找方法定义。作者证明翻译结果程序与其源 FGG− 程序具有相同动态语义，证明基于语法化的、步索引的逻辑关系；步索引在递归接口类型和递归方法下保证关系良基。翻译虽非确定性，但具有一致性（coherence）。
Abstract 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 ${\textrm{FGG}^{-}}$ to an untyped lambda-calculus. ${\textrm{FGG}^{-}}$ includes all features of FGG but type assertions. The translation of an ${\textrm{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 ${\textrm{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.
@article{paperbot2144,
title = {A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go},
author = {MARTIN SULZMANN and STEFAN WEHR},
journal = {Journal of Functional Programming},
volume = {33},
year = {2023},
doi = {10.1017/s0956796823000047}
}