米兰体育 研究 HOL 中的 ML 模块系统

引用

Gunter EL 和 Maharaj S (1995) 研究 HOL 中的 ML 模块系统。计算机杂志，38 (2)，第 142-151 页。 https://doi.org/10.1093/comjnl/38.2.142

摘要
在 VanInwegen 和 Gunter 的早期项目中，标准 ML (SML) 核心的动态语义被编码在 HOL 定理证明器中。我们通过添加动态模块系统来扩展它。然后，我们为具有高阶函子的模块系统开发可能的动态语义，并对其进行编码。接下来，我们通过嵌入和投影将这两种语义联系起来，并讨论如何使用它们来证明所提出的系统中的评估是 SML 模块系统中评估的保守扩展（在适当的意义上）。

期刊
计算机杂志：第 38 卷，第 2 期