$\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.

翻译：$\text{TT}^{\Box}_{{\mathcal C}}$ 是一个由模态参数化、具有有效性且满足外延性的类型论泛型族，其具备力迫解释。本文识别了 $\text{TT}^{\Box}_{{\mathcal C}}$ 理论的一个子类，该子类通过状态性计算（如引用单元）内部实现了连续性原理。连续性原理是系统T等若干直觉主义理论所具备的奠基性性质，其大致含义为：实数上的函数仅需这些数的近似值即可进行计算。通常连续性原理通过语义论证得以确立，但已知函数的连续模数可通过异常或引用单元等有效计算来求取。本文利用理论内部启用的状态性计算，直接计算了贝尔空间上泛函的连续模数。