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 pi-calculus, which generalizes Sangiorgi's work. To achieve this aim, we introduce indexed higher order pi-calculus, which is similar to higher order pi-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. (c) 2012 Elsevier B.V. All rights reserved.