$\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 等多个直觉主义理论所具有的基本性质。粗略地说，它指出实数上的函数仅需这些数的近似值即可计算。通常，连续性原理通过语义论证得以证明，但已知函数的连续模可以利用诸如异常或引用单元等效应计算来求得。在本文中，贝尔空间上泛函的连续模直接利用该理论内部启用的状态化计算进行计算。