Behavioral polymorphism and parametricity in session-based communication

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

34 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proceedings
Pages330-349
Number of pages20
Volume7792 LNCS
DOIs
Publication statusPublished - 2013
Event22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy
Duration: 16 Mar 201324 Mar 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7792 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
CountryItaly
CityRome
Period16/03/1324/03/13

Fingerprint

Dive into the research topics of 'Behavioral polymorphism and parametricity in session-based communication'. Together they form a unique fingerprint.

Cite this