Coq 中的 Martin-Löf 类型论
编程语言
2023-10-11 v1 计算机科学中的逻辑
摘要
我们展示了在 Coq 证明助手中对 Martin-Löf 类型论（MLTT）元理论的广泛机械化。我们的开发基于 Agda 中已有的工作，不仅展示了转换的可判定性，还利用双向类型检查引导的方法展示了类型检查的可判定性。从我们的可判定性证明中，我们获得了一个经过认证且可执行的类型检查器，支持 Π、Σ、ℕ 和恒等类型以及一个宇宙，适用于功能完备的 MLTT 版本。此外，我们的开发不依赖非谓词性、归纳-递归或任何超出带索引归纳类型模式和少量谓词性宇宙的 MLTT 之外的公理，从而将对象理论与元理论之间的差距缩小到仅为宇宙上的差异。最后，我们解释了我们的形式化选择，旨在依靠 Coq 的特性（例如由策略和宇宙多态性提供的元编程设施）实现模块化开发。
引用
@article{arxiv.2310.06376,
title = {Martin-L\"of \`a la Coq},
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
journal= {arXiv preprint arXiv:2310.06376},
year = {2023}
}