Bisimulation in name-passing calculi without matching

We study barbed equivalence in name-passing languages where there is no matching construct for testing equality between names. We concentrate on the π-calculus with capability types and subtypes, of which the untyped π-calculus without matching is a special case. We give a coinductive characterisation of typed barbed equivalence, and present “bisimulation up-to” techniques to enhance the resulting coinductive proof method. We then use these techniques to prove some process equalities that fail in the ordinary π-calculus