Showing 1–2 of 2 results for author: Jaramillo, J C

Contrasting Deadlock-Free Session Processes (Extended Version)

Authors: Juan C. Jaramillo, Jorge A. Pérez

Abstract: Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke etal's HCP, a type system based on a linear logic with hypersequen… ▽ More Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke etal's HCP, a type system based on a linear logic with hypersequents, and Padovani's priority-based type system for asynchronous processes, dubbed P. Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by HCP and P. We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency. △ Less

Submitted 25 April, 2025; v1 submitted 22 April, 2025; originally announced April 2025.

Comments: Full version of an ECOOP 25 paper

Around Classical and Intuitionistic Linear Processes

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

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 I… ▽ More 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. △ Less

Submitted 22 July, 2024; v1 submitted 8 July, 2024; originally announced July 2024.

Comments: Full version, 19 pages + appendices