Linear Logical Relations and Observational Equivalences for Session-Based Concurrency

(based on an ESOP'12 paper with Luís Caires, Frank Pfenning, and Bernardo Toninho)

In a prior work, Caires and Pfenning proposed an interpretation of intuitionistic linear logic propositions as session types for concurrent processes. The type system obtained from the interpretation ensures fundamental properties of session-based typed disciplines—most notably, type preservation, session fidelity, and global progress.

In this talk, I will present recent developments that complement and strengthen this interpretation. A first development is a theory of logical relations which is based on, and is remarkably similar to, that for functional languages, extended to an (intuitionistic) linear type structure. A main result is that well-typed processes always terminate (strong normalization). A second development is a notion of observational equivalence for session-typed processes. As applications, we prove that all proof conversions induced by the logic interpretation actually express observational equivalences, and explain how type isomorphisms resulting from linear logic equivalences are realized by coercions between interface types of session-based concurrent systems.