论文标题
高阶$ψ$ -calculi的通用类型系统
A Generic Type System for Higher-Order $Ψ$-calculi
论文作者
论文摘要
高阶$ψ$ -calculus框架（HO $ψ$）是对$π$ -Calculus的许多一阶和高阶扩展的概括。它是由Parrow等人提出的。他表明，诸如ho $π$和chocs之类的高阶微积分可以表示为ho $ψ$ -calculi。在本文中，我们提出了一个用于HO $ψ$ -CALCULI的通用类型系统，该系统扩展了Hüttel对一阶$ψ$ -calculi的通用类型系统的先前工作。我们的通用类型系统满足了降低受试者的通常属性，并且可以实例化以产生HOπ变体的类型系统，包括由于Demangeon等人而导致的终止类型系统。此外，我们得出了$ρ$ -CALCULUS的类型系统，这是Meredith和Radestock提出的反射性高阶演算。这就确定了我们的通用类型系统比其前身富裕，因为$ρ$ -calculus不能以满足编码标准标准的方式中编码$π$ -calculus。
The Higher-Order $Ψ$-calculus framework (HO$Ψ$) is a generalisation of many first- and higher-order extensions of the $π$-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HO$π$ and CHOCS can be expressed as HO$Ψ$-calculi. In this paper we present a generic type system for HO$Ψ$-calculi which extends previous work by Hüttel on a generic type system for first-order $Ψ$-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HOπ, including the type system for termination due to Demangeon et al. Moreover, we derive a type system for the $ρ$-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the $ρ$-calculus cannot be encoded in the $π$-calculus in a way that satisfies standard criteria of encodability.
