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.

29 pages

*CITI and Departamento de Informática, Faculdade de Ciências e Tecnologia,
Universidade Nova de Lisboa
**CITI and Departamento de Informática, Faculdade de Ciências e Tecnologia,
Universidade Nova de Lisboa, and Carnegie Mellon University

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu