Around Classical and Intuitionistic Linear Processes

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

19 Downloads (Pure)

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 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.

Original languageEnglish
Title of host publication35th International Conference on Concurrency Theory, CONCUR 2024
EditorsRupak Majumdar, Alexandra Silva
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Number of pages19
ISBN (Electronic)9783959773393
DOIs
Publication statusPublished - Sept-2024
Event35th International Conference on Concurrency Theory, CONCUR 2024 - Calgary, Canada
Duration: 9-Sept-202413-Sept-2024

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume311
ISSN (Print)1868-8969

Conference

Conference35th International Conference on Concurrency Theory, CONCUR 2024
Country/TerritoryCanada
CityCalgary
Period09/09/202413/09/2024

Keywords

  • linear logic
  • Process calculi
  • session types

Fingerprint

Dive into the research topics of 'Around Classical and Intuitionistic Linear Processes'. Together they form a unique fingerprint.

Cite this