Equivalence checking for a finite higher order π-calculus

Abstract

In this paper, we present an algorithm for checking weak context bisimulation over a finite higher order π-calculus, called linear higher order π-calculus. To achieve this aim, we propose a new bisimulation, called linear normal bisimulation, and furthermore prove the equivalence between context bisimulation and linear normal bisimulation for such linear higher order π-calculus. The correctness of this algorithm is also demonstrated. At last, we give a complete inference system for linear higher order π-calculus. © 2008 Springer-Verlag Berlin Heidelberg.