Decidable Fragments of a Higher Order Calculus with Locations

Homer is a higher order process calculus with locations. In this paper we study Homer in the setting of the semantic finite control property, which is a finite reachability criterion that implies decidability of barbed bisimilarity. We show that strong and weak barbed bisimilarity are undecidable for Homer. We then identify and compare two distinct subcalculi of Homer that both satisfy the semantic finite control property. One subcalculus is obtained by using a type system bounding the size of process terms. The other subcalculus is obtained by considering the image of the encoding of the finite control π-calculus in Homer.