文章

米兰体育 研究 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 期

状态已发布
发布日期31/12/1995
发布商牛津大学出版社
ISSN0010-4620
eISSN1460-2067

人 (1)

萨维·马哈拉吉博士

萨维·马哈拉吉博士

高级讲师,计算科学