The higher-order, call-by-value applied pi-calculus

Nobuyuki Sato, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)


We define a higher-order process calculus with algebraic operations such as encryption and decryption, and develop a bisimulation proof method for behavioral equivalence in this calculus. Such development has been notoriously difficult because of the subtle interactions among generative names, processes as data, and the algebraic operations. We handle them by carefully defining the calculus and adopting Sumii et al.'s environmental bisimulation, and thereby give (to our knowledge) the first "useful" proof method in this setting. We demonstrate the utility of our method through examples involving both higher-order processes and asymmetric cryptography.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Number of pages16
Publication statusPublished - 2009
Event7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of
Duration: 2009 Dec 142009 Dec 16

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5904 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
Country/TerritoryKorea, Republic of

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'The higher-order, call-by-value applied pi-calculus'. Together they form a unique fingerprint.

Cite this