Paper Info
Title
Linear logical relations and observational equivalences for session-based concurrency.
Abstract
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.
Year
DOI
Venue
2014
10.1016/j.ic.2014.08.001
Information and Computation
Keywords
Field
DocType
Session types,Linear logic,Process calculi,Strong normalization,Confluence,Logical relations,Observational equivalences
Discrete mathematics,Normalization (statistics),Functional programming,Concurrency,Observational equivalence,Correctness,Coinduction,Linear logic,Process calculus,Mathematics
Journal
Volume
Issue
ISSN
239
C
0890-5401
Citations 
PageRank 
References 
13
0.63
33
Authors
4
Name
Order
Citations
PageRank
Jorge A. Pérez122221.19
Luís Caires2103763.30
Frank Pfenning33376265.34
Bernardo Toninho420114.31