TY - GEN
T1 - The higher-order, call-by-value applied pi-calculus
AU - Sato, Nobuyuki
AU - Sumii, Eijiro
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=72449190044&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=72449190044&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-10672-9_22
DO - 10.1007/978-3-642-10672-9_22
M3 - Conference contribution
AN - SCOPUS:72449190044
SN - 3642106714
SN - 9783642106712
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 311
EP - 326
BT - Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
T2 - 7th Asian Symposium on Programming Languages and Systems, APLAS 2009
Y2 - 14 December 2009 through 16 December 2009
ER -