Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@techreport{Kouzapas:2015:10.25561/94985,
author = {Kouzapas, D and Pérez, JA and Yoshida, N},
booktitle = {Departmental Technical Report: 15/1},
doi = {10.25561/94985},
publisher = {Department of Computing, Imperial College London},
title = {Core higher-order session processes: tractable equivalences and relative expressiveness},
url = {http://dx.doi.org/10.25561/94985},
year = {2015}
}
Download

RIS format (EndNote, RefMan)

TY  - RPRT
AB  - This work proposes tractable bisimulations for the higher-order  -calculus with session primitives (HO ) and o ers a complete study of the expressivityof its most significant subcalculi. First we develop three typed bisimulations,which are shown to coincide with contextual equivalence. These characterisationsdemonstrate that observing as inputs only a specific finite set ofhigher-order values (which inhabit session types) su ces to reason about HO processes. Next, we identify HO, a minimal, second-order subcalculus of HO in which higher-order applications/abstractions, name-passing, and recursion areabsent. We show that HO can encode HO  extended with higher-order applicationsand abstractions and that a first-order session  -calculus can encode HO .Both encodings are fully abstract. We also prove that the session  -calculus withpassing of shared names cannot be encoded into HO  without shared names. Weshow that HO , HO, and   are equally expressive; the expressivity of HO enablese ective reasoning about typed equivalences for higher-order processes.
AU  - Kouzapas,D
AU  - Pérez,JA
AU  - Yoshida,N
DO  - 10.25561/94985
PB  - Department of Computing, Imperial College London
PY  - 2015///
TI  - Core higher-order session processes: tractable equivalences and relative expressiveness
T1  - Departmental Technical Report: 15/1
UR  - http://dx.doi.org/10.25561/94985
UR  - http://hdl.handle.net/10044/1/94985
ER  -
Download