在 Dedukti 中混合 HOL 与 Coq（扩展摘要）
计算机科学中的逻辑
2015-08-03 v1
摘要
我们将 Dedukti 用作实现互操作性的逻辑框架。我们利用自动化工具将 HOL 与 Coq 中完成的不同开发成果翻译至 Dedukti，并将其组合以证明新的结果。我们以一个具体示例阐明我们的方法：用 HOL 的自然数实例化 Coq 中编写的排序算法。
引用
@article{arxiv.1507.08721,
title = {Mixing HOL and Coq in Dedukti (Extended Abstract)},
author = {Ali Assaf and Raphaël Cauderlier},
journal= {arXiv preprint arXiv:1507.08721},
year = {2015}
}
备注
In Proceedings PxTP 2015, arXiv:1507.08375