ac米兰官方网站 研究 HOL 中的 ML 模块系统

引用

Maharaj S 和 Gunter EL (1994) 研究 HOL 中的 ML 模块系统。见：Melham T 和 Camilleri J（编辑）高阶逻辑定理证明及其应用：第七届国际研讨会，马耳他瓦莱塔，1994 年 9 月 19 日至 22 日会议记录。计算机科学讲义，859。第七届高阶逻辑定理证明及其应用国际研讨会，马耳他瓦莱塔，1994 年 9 月 19 日至 1994 年 9 月 22 日。柏林海德堡：Springer，第 346-361 页。 http://link.springer.com/chapter/10.1007/3-540-58450-1_53#； https://doi.org/10.1007/3-540-58450-1_53

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