我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：为 CIC 给出纯语法的 presheaf 模型，同时保持转换并解释完整依赖消去。

本文关注 Calculus of Inductive Constructions（CIC）的语义模型。已有类似 presheaf 模型往往难以同时兼顾转换（conversion）与完整的依赖消去。作者构造了一个纯语法的 presheaf 模型，并说明该变体能够保留转换，同时解释 full dependent elimination。摘要只给出两项结果中的第一项，未展开另一项结果；评估以模型构造和理论性质证明为主，未报告实现或实验。

问题

如何为 CIC 构造一个纯语法 presheaf 模型，并同时保留转换与解释完整的依赖消去。

方法

采用纯语法 presheaf 语义，构造 CIC 的模型变体。

评估

通过理论证明说明模型保留转换并解释 full dependent elimination；摘要未提及实验评估。

链接与引用

DOI 原文 ·

@inproceedings{paperbot5548,
  title = {Russian Constructivism in a Prefascist Theory},
  author = {Pierre-Marie Pédrot},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394740}
}