paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Reduction Free Normalisation for a proof irrelevant type of propositions

证明无关命题类型的无归约规范化
LMCS vol.Volume 19, Issue 32023匹配度 3/10 · 该论文属于类型论与证明助手基础理论，涉及规范化与转换可判定性，与形式化验证有间接关联；但用户核心方向是静态分析在 ML/Agentic 程序中的应用、LLM/Agent 改进静态分析与形式化验证、浮点或贝叶斯程序分析，本文既未涉及 LLM/Agent，也未涉及程序分析或具体验证工具落地，匹配度较低。引用 1 inbox
Thierry Coquand
类型系统
crossref: 2026-09-10

AI 速览

一句话：为含宇宙层级与证明无关命题的类型理论给出无归约规范化及转换可判定性证明，且无需显式中性与范式。

本文研究一个与 Lean 证明助手所用类型系统相近的类型理论，该理论包含宇宙层级以及证明无关的命题类型。作者证明该理论的规范化性质，并由此得到可转换性（convertibility）的可判定性。与以往论证不同，该证明不需要显式引入中性形式（neutral forms）与范式（normal forms）的概念，因此提供了一种“无归约”的规范化证明路径。关键结果是在证明无关命题与宇宙层级共存的情形下建立规范化并判定转换，为类似证明助手内核的类型检查与定义相等性判定提供了理论保证。

问题
研究含宇宙层级和证明无关命题类型的类型理论中，规范化性质是否成立以及可转换性是否可判定。
方法
给出一个不显式引入中性形式和范式概念的规范化证明，并据此推导可转换性的可判定性。
评估
通过类型论元理论证明而非实验评估来验证结果：建立规范化，并推出转换关系可判定；与已有需要中性/范式概念的论证形成对照。
原文摘要（Abstract）

We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot2205,
  title = {Reduction Free Normalisation for a proof irrelevant type of propositions},
  author = {Thierry Coquand},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 3},
  year = {2023},
  doi = {10.46298/lmcs-19(3:5)2023}
}