Around Classical and Intuitionistic Linear Processes

TL;DR

This paper explores the formal relationship between two families of session type systems derived from intuitionistic and classical linear logic, providing formal links through translation and full abstraction results.

Contribution

It offers the first formal analysis connecting intuitionistic and classical linear logic-based session type systems using translation and observational equivalence.

Findings

Established full abstraction results for the translation from CLL to ILL

Provided formal links between different type systems for concurrency

Clarified the relationship between intuitionistic and classical linear processes

Abstract

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent (2018), we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey (2017). Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.