Paper Info
Title
Full abstraction in a subtyped pi-calculus with linear types
Abstract
We introduce a concise pi-calculus with directed choices and develop a theory of subtyping. Built on a simple behavioural intuition, the calculus offers exact semantic analysis of the extant notions of subtyping in functional programming languages and session-based programming languages. After illustrating the idea of subtyping through examples, we show type-directed embeddings of two known subtyped calculi, one for functions and another for session-based communications. In both cases, the behavioural content of the original subtyping is precisely captured in the fine-grained subtyping theory in the pi-calculus. We then establish full abstraction of these embeddings with respect to their standard semantics, Morris's contextual congruence in the case of the functional calculus and testing equivalence for the concurrent calculus. For the full abstraction of the embedding of the session-based calculus, we introduce a new proof method centring on non-deterministic computational adequacy and definability. Partially suggested by a technique used by Quaglia and Walker for their full abstraction result, the new proof method extends the framework used in game-based semantics to the May/Must equivalences, giving a uniform proof method for both deterministic and non-deterministic languages.
Year
DOI
Venue
2011
10.1007/978-3-642-23217-6_19
CONCUR
Keywords
Field
DocType
full abstraction result,full abstraction,functional calculus,session-based communication,session-based calculus,original subtyping,new proof method,linear type,subtyped pi-calculus,subtyped calculus,concurrent calculus,fine-grained subtyping theory
Discrete mathematics,Functional calculus,Programming language,Embedding,Abstraction,Functional programming,Computer science,Theoretical computer science,Equivalence (measure theory),Subtyping,Congruence (geometry),Semantics
Conference
Volume
ISSN
Citations 
6901
0302-9743
30
PageRank 
References 
Authors
1.24
18
2
Name
Order
Citations
PageRank
Romain Demangeon11227.80
Kohei Honda269829.60