文章
详情
引用
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 |
发布商 | 牛津大学出版社 |
ISSN | 0010-4620 |
eISSN | 1460-2067 |
人 (1)
高级讲师,计算科学