$ext{TT}^{Box}\_{{mathcal C}}$: 一族具有连续效果实现的外延类型理论
摘要：在本文中，我们介绍了一种名为 $ ext{TT}^{Box}\_{{mathcal C}}$ 的泛型家族，它是一种具有强制解释参数化的增强型外延类型理论，这种参数化由模态性决定。我们确定了 $ ext{TT}^{Box}\_{{mathcal C}}$ 理论中能够通过状态化计算（例如引用单元）内部实现连续性原理的子类。连续性原理是一种对于一些直觉主义理论（如 System T）非常重要的性质。大致而言，它说明实数函数只需要通过对这些实数的逼近来进行计算。通常，连续性原理是通过语义论证来进行验证的，但我们知道可以通过引用单元等有副作用的计算来计算函数的连续性限度。在本文中，我们直接使用在理论内部启用的状态化计算来计算贝尔空间上的函数式的连续性限度。
作者：Liron Cohen and Vincent Rahli
论文ID：2307.14168
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-27