• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >The Definitional Side of the Forcing
【24h】

The Definitional Side of the Forcing

机译：强迫的定义面

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper studies forcing translations of proofs in dependent type theory, through the Curry-Howard correspondence. Based on a call-by-push-value decomposition, we synthesize two simply-typed translations: i) one call-by-value, corresponding to the translation derived from the presheaf construction as studied in a previous paper; ii) one call-by-name, whose intuitions already appear in Krivine and Miquel's work. Focusing on the call-by-name translation, we adapt it to the dependent case and prove that it is compatible with the definitional equality of our system, thus avoiding coherence problems. This allows us to use any category as forcing conditions, which is out of reach with the call-by-value translation. Our construction also exploits the notion of storage operators in order to interpret dependent elimination for inductive types. This is a novel example of a dependent theory with side-effects, clarifying how dependent elimination for inductive types must be restricted in a non-pure setting. Being implemented as a Coq plugin, this work gives the possibility to formalize easily consistency results, for instance the consistency of the negation of Voevodsky's univalence axiom.
机译：本文通过Curry-Howard对应关系研究了依赖类型理论中的强制证明翻译。基于按值调用分解，我们合成了两种简单类型的翻译：i）一个按值调用，对应于从前一篇论文中研究的presheaf结构派生的翻译; ii）一个叫人的名字，其直觉已经出现在Krivine和Miquel的作品中。着重于按名称呼叫转换，我们将其适应于依从情况，并证明其与我们系统的定义相等性兼容，从而避免了连贯性问题。这使我们可以使用任何类别作为强制条件，而按值调用转换则无法达到这一条件。我们的构造还利用存储运算符的概念来解释归纳类型的依存消除。这是具有副作用的依存理论的一个新颖示例，阐明了在非纯环境中必须限制对归纳类型的依存消除。作为Coq插件实现，这项工作使轻松地将一致性结果（例如对Voevodsky的单调公理的否定一致）的形式化成为可能。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号