2026-08-10T10:38:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20802 2024-08-29T05:40:58Z ddc:004 open_access

Around Classical and Intuitionistic Linear Processes Jaramillo, Juan C. Frumin, Dan Pérez, Jorge A. Process calculi session types linear logic Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical 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, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Juan C. Jaramillo and Dan Frumin and Jorge A. Pérez 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.30 urn:nbn:de:0030-drops-208026 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.30 eng https://creativecommons.org/licenses/by/4.0/legalcode