论文标题
Isabelle中的同喻类型理论
Homotopy Type Theory in Isabelle
论文作者
论文摘要
本文介绍了Isabelle/Hott，这是Isabelle证明助手中同型类型理论的第一个发展。在Paulson早期工作的基础上，我使用Isabelle现有的逻辑框架基础结构来实现基本自动化，例如类型检查和术语详细说明，通常在依赖类型系统的源代码级别上处理。我还将命题-AS类型范式与声明性的ISAR证明语言相结合，为基于策略的COQ证明和AGDA的证明条款提供了替代方案。然后，开发的基础架构用于正式化同型理论书籍的基础结果。
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.
