CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms

Abstract

We propose a general definition of higher-order process calculi, generalizing CHOCS [Tho89] and related calculi, and investigate its basic properties. We give sufficient conditions under which a calculus is finitely-branching and effective. We show that a suitable notion of higher-order bisimulation is a congruence for a subclass of higher-order calculi. We illustrate our definitions with a simple calculus strictly stronger than CHOCS.