Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Around Classical and Intuitionistic Linear Processes

Juan C. Jaramillo, Dan Frumin, Jorge A. Pérez

TL;DR

The paper addresses how intuitionistic and classical linear-process type systems, rooted in Curry–Howard correspondences between linear logic and session types, formally relate to each other. It grounds this relation in Laurent's translation from $CLL$ to $ILL$ and Atkey's observational equivalence, then strengthens the connection by establishing denotational and operational full abstractions between the two realms. By lifting Laurent's translation to denotations and encoding it as transformer contexts, the authors show that the classical-process semantics and their translated intuitionistic counterparts are indistinguishable under observation, and that this equivalence can be preserved under composition via mediating synchronizers. The results provide a rigorous bridge between disparate yet related type systems for concurrency, clarifying formal links and enabling cross-pollination between classical and intuitionistic session-type frameworks. They also open avenues for applying these insights to other semantic models and language implementations that draw on linear logic and session types.

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.

Around Classical and Intuitionistic Linear Processes

TL;DR

The paper addresses how intuitionistic and classical linear-process type systems, rooted in Curry–Howard correspondences between linear logic and session types, formally relate to each other. It grounds this relation in Laurent's translation from to and Atkey's observational equivalence, then strengthens the connection by establishing denotational and operational full abstractions between the two realms. By lifting Laurent's translation to denotations and encoding it as transformer contexts, the authors show that the classical-process semantics and their translated intuitionistic counterparts are indistinguishable under observation, and that this equivalence can be preserved under composition via mediating synchronizers. The results provide a rigorous bridge between disparate yet related type systems for concurrency, clarifying formal links and enabling cross-pollination between classical and intuitionistic session-type frameworks. They also open avenues for applying these insights to other semantic models and language implementations that draw on linear logic and session types.

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.
Paper Structure (9 sections, 6 theorems, 29 equations, 10 figures, 1 table)

This paper contains 9 sections, 6 theorems, 29 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Laurent's Translation ${(-)}^{\bullet}_\mathsf{R}$.
  4. A Denotational Characterization of Laurent's Translation
  5. The Composed Translation.
  6. The Translation on Processes.
  7. Properties.
  8. An Operational Characterization of Laurent's Translation
  9. Concluding Remarks

Key Result

Theorem 2

If $C\mathrel{\vdash^{{c}}} \cdot \;|\; \Theta$, then $C\Downarrow \theta$ iff $\theta \in\textcolor{RedOrange}{\llbracket}C\mathrel{\vdash^{{c}}} \cdot\;|\; \Theta\textcolor{RedOrange}{\rrbracket}$.

Figures (10)

  • Figure 1: Translations between $\mathcal{\textsf{CLL}}$ and $\mathcal{\textsf{ILL}}$. In this paper, we shall fix $\mathsf{R} = \textbf{1}$.
  • Figure 2: Typing rules. $\mathcal{\textsf{CP}}\xspace$ does not include 'mix'. $\mathcal{\textsf{CP}}\xspace_{0}\xspace$ is $\mathcal{\textsf{CP}}\xspace + \textmd{{\TirNameStyle{Mix}}{}_0}\xspace$, $\mathcal{\textsf{CP}}\xspace_{02}\xspace$ is $\mathcal{\textsf{CP}}\xspace_{0}\xspace + \textmd{{\TirNameStyle{Mix}}{}_2}\xspace$.
  • Figure 3: Classical Processes: Configurations.
  • Figure 4: Classical Processes: Observations.
  • Figure 5: Classical Processes: Denotational Semantics
  • ...and 5 more figures

Theorems & Definitions (16)

  • Definition 1: Observational equivalence ObservationsCP
  • Theorem 2: Adequacy ObservationsCP
  • Corollary 3: ObservationsCP
  • Remark 4
  • Theorem 5: Laurent
  • Lemma 6: Laurent
  • Definition 7: Synchronizer
  • Definition 8: Laurent's translation on processes
  • Example 9
  • Definition 10: Transformations on Denotations
  • ...and 6 more