Observed communication semantics for classical processes

Atkey, Robert; Yang, Hongseok, ed. (2017) Observed communication semantics for classical processes. In: Programming Languages and Systems. Lecture Notes in Computer Science . Springer, SWE, pp. 56-82. (https://doi.org/10.1007/978-3-662-54434-1_3)

[thumbnail of Atkey-ESOP2017-Observed-communication-semantics-for-classical-processes]
Preview
 Text. Filename: Atkey_ESOP2017_Observed_communication_semantics_for_classical_processes.pdf
Accepted Author Manuscript
Download (436kB)| Preview

Abstract

Classical Linear Logic (CLL) has long inspired readings of its proofs as communicating processes. Wadler's CP calculus is one of these readings. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence. We propose a new operational semantics for CP based on the idea of observing communication, and use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, we use the standard relational denotational semantics of CLL. We show that this denotational semantics is adequate for our operational semantics. This allows us to deduce that, for instance, all the cut-elimination rules of CLL are observational equivalences.

CORE (COnnecting REpositories)