一句话：提出一族外延类型理论，可在系统内用引用单元等有状态计算直接实现连续性原则。
论文研究如何在类型论中为连续性原则提供计算性实现。连续性原则是 System T 等直觉主义理论的重要性质，粗略地说，实数上的函数只需实数的近似即可计算；传统上多通过语义论证证明。作者在 TT^□_C 这一由模态参数化、带力迫解释的效应化外延类型理论族中，识别出一个子类，使理论内部能通过引用单元等有状态计算实现连续性。进一步，Baire 空间上泛函的连续性模可由该理论内部启用的有状态计算直接得到，从而把连续性的实现从外部语义论证转向理论内部的效应化计算。
$\text{TT}^{\Box}_{{\mathcal C}}$ is a generic family of effectful, extensional type theories with a forcing interpretation parameterized by modalities. This paper identifies a subclass of $\text{TT}^{\Box}_{{\mathcal C}}$ theories that internally realizes continuity principles through stateful computations, such as reference cells. The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. In this paper, the modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled internally in the theory.
@article{paperbot2750,
title = {$\text{TT}^{\Box}_{\mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity},
author = {Liron Cohen and Vincent Rahli},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:18)2024}
}