An interpretation of Erlang into value-passing Calculus

H. Huang, F. Yang

Research output: Contribution to journalArticleAcademicpeer-review

172 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)1504-1513
Number of pages10
JournalJournal of Networks
Issue number7
Publication statusPublished - 2013
Externally publishedYes


  • Symbolic bisimulation
  • Value-passing calculus
  • Verification


Dive into the research topics of 'An interpretation of Erlang into value-passing Calculus'. Together they form a unique fingerprint.

Cite this