We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types, based on a combination of guarded recursion and impredicative polymorphism; because our model is based on recursively defined semantic worlds, it is compatible with polymorphism and relational reasoning about stateful abstract datatypes. We then extend our language with modal constructs for proof-relevant relational reasoning based on the "logical relations as types" principle, in which equivalences between imperative abstract datatypes can be established synthetically. What is new in relation to prior typed denotational models of higher-order store is that our Kripke worlds need not be syntactically definable, and are thus compatible with relational reasoning in the heap. Our work combines recent advances in the operational semantics of state with the purely denotational viewpoint of synthetic guarded domain theory.

翻译：我们提出了首个结合保护递归与逆变性多态性的多态依赖类型理论的指称语义，该语义扩展了关于通用（高阶）引用类型和递归类型的等式理论；由于我们的模型基于递归定义的语义世界，因此它与多态性以及关于有状态抽象数据类型的关系推理兼容。随后，我们基于“逻辑关系即类型”原则，在语言中扩展了用于证明相关关系推理的模态构造，从而能够综合性地建立命令式抽象数据类型之间的等价关系。与以往高阶存储的类型化指称模型相比，本工作的创新之处在于：我们的克里普克世界无需语法可定义，因此与堆中的关系推理兼容。本研究将状态操作语义的最新进展与合成保护域理论的纯指称视角相结合。