More on bisimulations for higher order π-calculus

In this paper, we prove the coincidence between strong/weak context bisimulation and strong/weak normal bisimulation for higher order π-calculus, which generalizes Sangiorgi’s work. To achieve this aim, we introduce indexed higher order π-calculus, which is similar to higher order π-calculus except that every prefix of any process is assigned indices. Furthermore we present corresponding indexed bisimulations for this calculus, and prove the equivalence between these indexed bisimulations. Based on this result, we prove the main result of this paper, i.e., the equivalence between strong/weak context bisimulation and strong/weak normal bisimulation.