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.

翻译：线性逻辑（LL）与会话类型之间的Curry-Howard对应为并发过程提供了坚实基础。由于该对应关系同时适用于直觉主义与经典版本的线性逻辑（ILL与CLL），我们获得了两个不同的并发类型系统族。一个悬而未决的问题是：这两个类型系统族之间究竟存在何种精确关联？基于Laurent（2018）提出的从CLL到ILL的转换方法，我们借助Atkey（2017）提出的类型化观测等价理论，以完全抽象结果的形式给出了两个互补的答案。我们的研究结果揭示了看似相关实则不同的并发类型系统之间迄今缺失的形式化联系。