paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Stack semantics of type theory

类型论的栈语义
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 1/10 · 该论文研究依赖类型论的栈语义与泛等宇宙模型，属于纯类型论/形式语义，与用户关注的静态分析、Agentic 程序分析、浮点程序分析、贝叶斯程序分析及 LLM 交叉方向几乎无直接关联。引用 31 inbox
Thierry Coquand, Bassel Mannaa, Fabian Ruch
形式语义
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：用栈模型解释带一个泛等宇宙与命题截断的依赖类型论，并证明可数选择不可证。

本文研究依赖类型论中一个泛等宇宙与命题截断的语义。作者构造了一个模型，将类型解释为栈（stack），这是对类型论 groupoid 模型的推广。通过该栈语义，依赖类型论中的类型获得相应语义结构，并可用于分析带一个泛等宇宙和命题截断的系统。作为应用，作者证明可数选择（countable choice）在该依赖类型论中不可证明。这一结果说明，即使加入一个泛等宇宙和命题截断，可数选择仍不能被推出，从而给出了该类型论中截断与选择原理之间的独立性。

问题
为带一个泛等宇宙与命题截断的依赖类型论提供语义模型，并判断可数选择在该理论中是否可证。
方法
将类型解释为栈，推广类型论的 groupoid 模型，构造出相应的依赖类型论模型。
评估
在该栈语义模型下证明：可数选择在带一个泛等宇宙与命题截断的依赖类型论中不可证明。
原文摘要（Abstract）

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

链接与引用

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

BibTeX 
@inproceedings{CoquandMR17,
  title = {Stack semantics of type theory},
  author = {Thierry Coquand and Bassel Mannaa and Fabian Ruch},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005130}
}