Abstract

Classical Linear Logic (CLL) has long inspired readings of its proofs as concurrent processes. Wadler’s CP calculus is one of these readings that views the formulas of CLL as session types and proofs as processes. 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.

In this talk, I will propose a new operational semantics for CP based on the idea of observing communication between communicating processes. I’ll use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, I use of the standard relational denotational semantics of CLL . This denotational semantics is adequate for our operational semantics, and enables a proof that all the cut-elimination rules of CLL are observational equivalences.