# Observed Communication Semantics for Classical Processes

## Publication Information

Robert Atkey.

*Observed Communication Semantics for Classical Processes*. In Hongseok Yang, editor,

*Programming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017*, volume 10201 of

*Lecture Notes in Computer Science*, pages 56-82. 2017.

DOI:

10.1007/978-3-662-54434-1_3## 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.