类型论的栈语义
计算机科学中的逻辑
2017-04-21 v2
摘要
我们给出一个具有一个单值宇宙和命题截断的依值类型论模型，该模型将类型解释为栈，推广了类型论的广群模型。作为一个应用，我们证明了可数选择在具有一个单值宇宙和命题截断的依值类型论中无法被证明。
引用
@article{arxiv.1701.02571,
title = {Stack Semantics of Type Theory},
author = {Thierry Coquand and Bassel Mannaa and Fabian Ruch},
journal= {arXiv preprint arXiv:1701.02571},
year = {2017}
}