We study the Higher-Order Ψ-calculi (HOΨ) of Parrow et al.: a general framework for representing many variants and extensions of the first- and higher-order π-calculi. Each specific calculus is obtained by setting and varying a small number of parameters; notably, the terms (channels) M, N, conditions φ, and assertions Ψ of the language, which are nominal data types, and an entailment relation Ψ ⊩ φ for controlling in which environments Ψ a condition φ, such as the equivalence between two channels, M, N , holds.
We review the syntax and labelled semantics, and we furthermore create three different reduction semantics for the HOΨ-calculus: One is fully compositional and uses structural congruence, but does not fully match every τ-labelled transition; the second matches this relation exactly but uses reduction contexts in place of structural rules; and the last is larger than the τ-transition relation and employs an evaluation relation rather than structural congruence directly.
Higher-order process mobility appears as a limited form of the more general capability of reflection; the generic ability of a program to turn code into data, compute with it, even modify it, and reinstantiate it as running code. We explore this connexion by showing that the HOΨ-framework can even represent the Reflective Higher-Order (RHO or ρ) calculus of Meredith and Radestock.
We define a generic type system for HOΨ, using the largest of the three reduction semantics, which thus encompasses all τ-labelled transitions. It includes generic rules for type judgements of processes, but requires type judgements for terms, conditions and assertions to be given as parameters, mirroring the fact that these sets are also parameters in the HOΨ-calculus. We prove a general result of subject reduction for the generic type system, but we cannot prove safety, since this relies on a notion of type error which will depend on the specific choice of parameter setting for the terms, conditions and assertions. Safety must therefore be proved manually for each instantiation.
Lastly, we attempt to type reflection, by instantiating the generic type system to the representation of the ρ-calculus. The example hints at the kinds of limitation that must be imposed on reflection to make it typable, such as including type information in the definition of entailment, to create a typed channel equivalence.