A generic type system for higher-order Ψ-calculi

Abstract

The Higher-Order Ψ-calculus framework (HOΨ) by Parrow et al. is a generalisation of many first- and higher-order extensions of the π-calculus. In this paper we present a generic type system for HOΨ-calculi. It satisfies a subject reduction property and can be instantiated to yield both existing and new type systems for calculi, that can be expressed as HOΨ-calculi. In this paper, we consider the type system for termination in HOπ by Demangeon et al. Moreover, we derive a new type system for the ρ-calculus of Meredith and Radestock and present a type system for non-interference for mobile code.