Characteristic bisimulation for higher-order session processes
File(s)5.pdf (597.83 KB)
Published version
Author(s)
Kouzapas, D
Yoshida, N
Perez, J
Type
Conference Paper
Abstract
Characterising contextual equivalence is a long-standing issue for higher-order (process) languages. In the setting of a higher-order pi-calculus with sessions, 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
2015-12-31
Date Acceptance
2015-06-15
Citation
26th International Conference on Concurrency Theory (CONCUR 2015), 2015, 42, pp.398-411
ISBN
978-3-939897-91-0
ISSN
1868-8969
Publisher
Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH
Start Page
398
End Page
411
Journal / Book Title
26th International Conference on Concurrency Theory (CONCUR 2015)
Volume
42
Copyright Statement
© Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida 2015. Licensed under Creative Commons License CC-BY.
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
Source
26th International Conference on Concurrency Theory (CONCUR 2015)
Publication Status
Published
Start Date
2015-09-01
Finish Date
2015-09-04
Coverage Spatial
Madrid, Spain