Paper Info
Title
Behavioral polymorphism and parametricity in session-based communication
Abstract
We investigate a notion of behavioral genericity in the context of session type disciplines. To this end, we develop a logically motivated theory of parametric polymorphism, reminiscent of the Girard-Reynolds polymorphic λ-calculus, but casted in the setting of concurrent processes. In our theory, polymorphism accounts for the exchange of abstract communication protocols and dynamic instantiation of heterogeneous interfaces, as opposed to the exchange of data types and dynamic instantiation of individual message types. Our polymorphic session-typed process language satisfies strong forms of type preservation and global progress, is strongly normalizing, and enjoys a relational parametricity principle. Combined, our results confer strong correctness guarantees for communicating systems. In particular, parametricity is key to derive non-trivial results about internal protocol independence, a concurrent analogous of representation independence, and non-interference properties of modular, distributed systems.
Year
DOI
Venue
2013
10.1007/978-3-642-37036-6_19
ESOP
Keywords
Field
DocType
individual message type,motivated theory,behavioral polymorphism,data type,session-based communication,girard-reynolds polymorphic,dynamic instantiation,polymorphic session-typed process language,parametric polymorphism,polymorphism account,internal protocol independence,concurrent process,polymorphism,communication protocol,satisfiability,distributed system
Programming language,Computer science,Correctness,Parametric polymorphism,Theoretical computer science,Cloud server,Data type,Polymorphism (computer science),Modular design,Parametricity,Communications protocol
Conference
Volume
ISSN
Citations 
7792
0302-9743
20
PageRank 
References 
Authors
0.76
20
4
Name
Order
Citations
PageRank
Luís Caires1103763.30
Jorge A. Pérez222221.19
Frank Pfenning33376265.34
Bernardo Toninho420114.31