Comparing Session Type Systems derived from Linear Logic
CoRR(2024)
摘要
Session types are a typed approach to message-passing concurrency, where
types describe sequences of intended exchanges over channels. Session type
systems have been given strong logical foundations via Curry-Howard
correspondences with linear logic, a resource-aware logic that naturally
captures structured interactions. These logical foundations provide an elegant
framework to specify and (statically) verify message-passing processes.
In this paper, we rigorously compare different type systems for concurrency
derived from the Curry-Howard correspondence between linear logic and session
types. We address the main divide between these type systems: the classical and
intuitionistic presentations of linear logic. Along the years, these
presentations have given rise to separate research strands on logical
foundations for concurrency; the differences between their derived type systems
have only been addressed informally.
To formally assess these differences, we develop π𝖴𝖫𝖫, a session
type system that encompasses type systems derived from classical and
intuitionistic interpretations of linear logic. Based on a fragment of Girard's
Logic of Unity, π𝖴𝖫𝖫 provides a basic reference framework: we
compare existing session type systems by characterizing fragments of
π𝖴𝖫𝖫 that coincide with classical and intuitionistic formulations.
We analyze the significance of our characterizations by considering the
locality principle (enforced by intuitionistic interpretations but not by
classical ones) and forms of process composition induced by the
interpretations.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要