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)

Abstract

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
Pages311-326
Number of pages16
DOIs
Publication statusPublished - 2009 Dec 28
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

Other

Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
CountryKorea, Republic of
CitySeoul
Period09/12/1409/12/16

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this