Featherweight Go 的类型导向翻译方案之语义保持
编程语言
2022-06-22 v1
摘要
Featherweight Go（FG）是一种极简核心演算，包含重载方法与接口类型等 Go 语言基本特性。对 FG 程序动态行为最直白的语义描述是依据运行时类型信息来解析方法调用。一种更高效的方法是应用类型导向的翻译方案，其中接口值被替换为包含具体方法定义的字典。由此，方法调用可通过在字典中简单查找方法定义来解析。确立经类型导向翻译方案所得的目标程序保持原 FG 程序语义是一项重要任务。为确立该性质，我们采用按类型索引的逻辑关系来关联源程序与目标程序。我们提供了严格的证明，并详细讨论了所遭遇的诸多微妙之处，包括因递归接口与方法定义而需引入步索引。
引用
@article{arxiv.2206.09980,
title = {Semantic preservation for a type directed translation scheme of Featherweight Go},
author = {Martin Sulzmann and Stefan Wehr},
journal= {arXiv preprint arXiv:2206.09980},
year = {2022}
}
备注
38 pages, includes appendix with full proofs