A Generic Type System for Higher-Order $\Psi$-calculi

TL;DR

This paper introduces a versatile type system for Higher-Order $ ext{ extPsi}$-calculi, enabling consistent typing across various higher-order process calculi and extending previous type systems to more expressive frameworks.

Contribution

It presents a generic type system for HO$ extPsi$-calculi that satisfies subject reduction and can be instantiated for multiple variants, including the $ ho$-calculus.

Findings

Type system satisfies subject reduction property.

Can be instantiated for variants of HO$ extpi$ including termination.

Richer than previous systems, applicable to the $ ho$-calculus.

Abstract

The Higher-Order $\Psi$-calculus framework (HO$\Psi$) is a generalisation of many first- and higher-order extensions of the $\pi$-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HO$\pi$ and CHOCS can be expressed as HO$\Psi$-calculi. In this paper we present a generic type system for HO$\Psi$-calculi which extends previous work by H\"uttel on a generic type system for first-order $\Psi$-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HO{\pi}, including the type system for termination due to Demangeon et al. Moreover, we derive a type system for the $\rho$-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 $\rho$-calculus cannot be encoded in the $\pi$-calculus in a way that satisfies standard criteria of encodability.