论文标题
综合商店和多态性的典型语义
Denotational semantics of general store and polymorphism
论文作者
论文摘要
我们基于对一般（高阶）参考类型和递归类型扩展的多态性依赖性类型理论的第一个词语语义，基于守护的递归和不可思议的多态性的结合；由于我们的模型基于递归定义的语义世界，因此它与有关状态抽象数据类型的多态性和关系推理兼容。然后，我们使用模态构造扩展了语言，以基于“逻辑关系为类型”原理进行证明相关的关系推理，其中可以合成的急切抽象数据类型之间的等价。与先前的高阶商店键入典型词模型有关的是，我们的kripke世界不必在句法上定义，因此与堆中的关系推理兼容。我们的作品结合了国家运作语义的最新进展，以及纯粹的合成保护领域理论的观点。
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.
