Linear logical relations and observational equivalences for session-based concurrency

We investigate strong normalization, confluence, and behavioral equality in the realm of session-based concurrency. These interrelated issues underpin advanced correctness analysis in models of structured communications. The starting point for our study is an interpretation of linear logic propositi...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2014-12, Vol.239, p.254-302
Main Authors: Pérez, Jorge A., Caires, Luís, Pfenning, Frank, Toninho, Bernardo
Format: Article
Language:English
Subjects:
Confluence
Linear logic
Logical relations
Observational equivalences
Process calculi
Session types
Strong normalization
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We investigate strong normalization, confluence, and behavioral equality in the realm of session-based concurrency. These interrelated issues underpin advanced correctness analysis in models of structured communications. The starting point for our study is an interpretation of linear logic propositions as session types for communicating processes, proposed in prior work. Strong normalization and confluence are established by developing a theory of logical relations. Defined upon a linear type structure, our logical relations remain remarkably similar to those for functional languages. We also introduce a natural notion of observational equivalence for session-typed processes. Strong normalization and confluence come in handy in the associated coinductive reasoning: 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.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2014.08.001