摘要：In this paper we present a new process calculus VPC and an interpretation for core Erlang. VPC is at least as expressive as VPC and it is more effective for verification with some built-in functions. The wellestablished symbolic bisimulation in value-passing calculus is now helpful for solving the infinite-state space problem of data values in equivalence checking and verfication. Compared to the previous formalization work of modeling core Erlang in -calculus, the new interpretation has the following main merits: some essential features for Erlang are implemented faithfully; and above all the soundness of the interpretation is proved with respect to late symbolic bisimulation.
