Around Classical and Intuitionistic Linear Processes
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929428578172928 |
|---|---|
| author | Jaramillo, Juan C. Frumin, Dan Pérez, Jorge A. |
| author_facet | Jaramillo, Juan C. Frumin, Dan Pérez, Jorge A. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_06391 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Around Classical and Intuitionistic Linear Processes Jaramillo, Juan C. Frumin, Dan Pérez, Jorge A. Logic in Computer Science 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. |
| title | Around Classical and Intuitionistic Linear Processes |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.06391 |