高阶$\Psi$-演算的泛型类型系统

Alex Rønning Bendixen; Bjarke Bredow Bojesen; Hans Hüttel; Stian Lybech

doi:10.4204/EPTCS.368.3

高阶$\Psi$-演算的泛型类型系统

计算机科学中的逻辑 2022-09-07 v1 编程语言

作者: Alex Rønning Bendixen , Bjarke Bredow Bojesen , Hans Hüttel , Stian Lybech

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

高阶 $\Psi$ -演算框架（HO $\Psi$ ）是 $\pi$ -演算的许多一阶与高阶扩展的推广。它由Parrow等人提出，他们展示了HO $\pi$ 与CHOCS等高阶演算可表达为HO $\Psi$ -演算。本文我们提出一种用于HO $\Psi$ -演算的泛型类型系统，扩展了H\"uttel此前关于一阶 $\Psi$ -演算泛型类型系统的工作。我们的泛型类型系统满足主语归约（subject reduction）的通常性质，并可实例化以给出HO{\pi}变体的类型系统，包括Demangeon等人的终止性类型系统。此外，我们推导了 $\rho$ -演算（Meredith与Radestock提出的一种反射式高阶演算）的类型系统。这表明我们的泛型类型系统比其前驱更丰富，因为 $\rho$ -演算无法以满足可编码性标准准则的方式编码进 $\pi$ -演算。

关键词

高阶$\Psi$-演算泛型类型系统主语归约 $\rho$-演算 $\pi$-演算可编码性

引用

@article{arxiv.2209.02354,
  title  = {A Generic Type System for Higher-Order $\Psi$-calculi},
  author = {Alex Rønning Bendixen and Bjarke Bredow Bojesen and Hans Hüttel and Stian Lybech},
  journal= {arXiv preprint arXiv:2209.02354},
  year   = {2022}
}

备注

In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777

高阶$\Psi$-演算的泛型类型系统

摘要

关键词

引用

备注

相关论文