Isabelle/Pure中同伦类型理论的实现
计算机科学中的逻辑
2019-11-04 v1 逻辑
摘要
在本硕士论文中，我们给出了“书本HoTT”的一个片段作为交互式证明辅助工具Isabelle的对象逻辑的实现。我们也给出了Isabelle/Pure逻辑框架底层理论的数学描述，并讨论了当试图将带宇宙(intensional dependent type theory with universes)的内涵依赖类型论编码进简单类型论逻辑基础时出现的各种问题与设计决策。
引用
@article{arxiv.1911.00399,
title = {An Implementation of Homotopy Type Theory in Isabelle/Pure},
author = {Joshua Chen},
journal= {arXiv preprint arXiv:1911.00399},
year = {2019}
}
备注
Masters thesis