A Generic Type System for Higher-Order ?-calculi

The Higher-Order ?-calculus framework (HO?) is a generalisation of many first-and higher-order extensions of the p-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HOp 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 Huttel 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 HOp, 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 p-calculus in a way that satisfies standard criteria of encodability.