在 $\lambda$$\Pi$-演算模理论中编码带证明无关性的谓词子类型

Gabriel Hondet; Frédéric Blanqui

doi:10.4230/LIPIcs.TYPES.2020.6

在 $\lambda$$\Pi$-演算模理论中编码带证明无关性的谓词子类型

计算机科学中的逻辑 2021-10-27 v1

作者: Gabriel Hondet , Frédéric Blanqui

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

$\lambda$ $\Pi$ -演算模理论是一种逻辑框架，其中可编码各种逻辑与类型系统，从而有助于基于这些逻辑与类型系统的证明系统的交叉验证与互操作。在本文中，我们展示了如何编码谓词子类型与证明无关性，这两者均为 PVS 证明辅助器的两个重要特性。我们证明了该编码是正确的，且编码后的证明可由 Dedukti 机械检查，Dedukti 是一个使用重写技术的 $\lambda$ $\Pi$ -演算模理论类型检查器。

关键词

$\lambda$$\Pi$-演算模理论谓词子类型证明无关性逻辑框架编码 Dedukti PVS

引用

@article{arxiv.2110.13704,
  title  = {Encoding of Predicate Subtyping with Proof Irrelevance in the $\lambda$$\Pi$-Calculus Modulo Theory},
  author = {Gabriel Hondet and Frédéric Blanqui},
  journal= {arXiv preprint arXiv:2110.13704},
  year   = {2021}
}

备注

TYPES 2020 wasn't held in Turin as planned because of the COVID-19 outbreak. TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Turino, Italy

在 $\lambda$$\Pi$-演算模理论中编码带证明无关性的谓词子类型

摘要

关键词

引用

备注

相关论文