Characteristic bisimulation for higher-order session processes
File(s)art%3A10.1007%2Fs00236-016-0289-7.pdf (1.34 MB)
Published version
Author(s)
Kouzapas, D
Perez, JA
Yoshida, N
Type
Journal Article
Abstract
For higher-order (process) languages, characterising contextual equivalence is a long-standing issue. In the setting of a higher-order \(\pi \)-calculus with session types, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.
Date Issued
2016-12-24
Date Acceptance
2016-11-29
Citation
Acta Informatica, 2016, 54 (3), pp.271-341
ISSN
1432-0525
Publisher
Springer Verlag (Germany)
Start Page
271
End Page
341
Journal / Book Title
Acta Informatica
Volume
54
Issue
3
Copyright Statement
© The Author(s) 2016. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (EPSRC)
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
N/A
612985
EP/N027833/1
Subjects
Science & Technology
Technology
Computer Science, Information Systems
Computer Science
PI-CALCULUS
FULL ABSTRACTION
CONCURRENCY
LINEARITY
SEMANTICS
PCF
Computation Theory & Mathematics
0803 Computer Software
0804 Data Format
0802 Computation Theory And Mathematics
Publication Status
Published