Computer Science Department
School of Computer Science, Carnegie Mellon University
Relational Parametricity for Polymorphic Session Types
Luís Caires*, Jorge A. Pérez*, Frank Pfenning, Bernardo Toninho**
We introduce a theory of polymorphic concurrent processes, which arises from an interpretation of second-order intuitionistic linear logic propositions as polymorphic session types, in the style of the Girard-Reynolds polymorphic λ-calculus. The interpretation naturally generalizes recent discoveries on the correspondence between linear logic propositions and session types. In our proposed theory, polymorphism accounts for the exchange of abstract communication protocols, and dynamic instantiation of heterogeneous interfaces. Well-typed processes enjoy a strong form of subject reduction (type preservation) and global progress, but also termination (strong normalization) and relational parametricity (representation independence). The latter two properties are obtained by adapting proof techniques in the functional setting to linear session types. Furthermore, we discuss a faithful encoding of System F into our polymorphic session calculus.