论文标题
迈向高阶数学操作语义
Towards a Higher-Order Mathematical Operational Semantics
论文作者
论文摘要
众所周知，众所周知，高阶语言中的组成性证明是涉及的，并且很难确保构图的一般语义框架。特别是，Turi和Plotkin的Bialgebraic抽象GSO框架已成功应用于获得一阶语言的现成的组成结果，到目前为止，不适用于高阶语言。在目前的工作中，我们开发了一个针对高阶语言的抽象GSO规范理论，实际上将Turi和Plotkin框架的核心原理转移到了高阶设置。在我们的理论中，高阶语言的运行语义是我们指定高阶GSOS法律的某些DIN自然转变表示的。我们给出了一个一般的构图结果，该结果适用于以这种方式指定的所有系统，并讨论如何滑雪微积分和$λ$ -calculus W.R.T.作为实例，获得了艾布拉姆斯基的应用二次化的强大变体。
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.
