Substructural Observed Communication Semantics

Ryan Kavanagh
(Carnegie Mellon University)

Session-types specify communication protocols for communicating processes, and session-typed languages are often specified using substructural operational semantics given by multiset rewriting systems. We give an observed communication semantics for a session-typed language with recursion, where a process's observation is given by its external communications. To do so, we introduce fair executions for multiset rewriting systems, and extract observed communications from fair process executions. This semantics induces an intuitively reasonable notion of observational equivalence that we conjecture coincides with semantic equivalences induced by denotational semantics, bisimulations, and barbed congruences for these languages.

In Ornela Dardha and Jurriaan Rot: Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS 2020), Online, 31 August 2020, Electronic Proceedings in Theoretical Computer Science 322, pp. 69–87.
Published: 27th August 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.322.7 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org