Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ...
Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that l...
Main Authors: | , , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | unknown |
Published: |
arXiv
2023
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.2309.12466 https://arxiv.org/abs/2309.12466 |
id |
ftdatacite:10.48550/arxiv.2309.12466 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.48550/arxiv.2309.12466 2023-11-05T03:40:51+01:00 Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... Sano, Chuta Kavanagh, Ryan Pientka, Brigitte 2023 https://dx.doi.org/10.48550/arxiv.2309.12466 https://arxiv.org/abs/2309.12466 unknown arXiv Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 Programming Languages cs.PL FOS Computer and information sciences Article article CreativeWork Preprint 2023 ftdatacite https://doi.org/10.48550/arxiv.2309.12466 2023-10-09T11:04:28Z Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as ... : Technical report containing an appendix with additional proofs. Companion to an OOPSLA'23 paper of the same name ... Article in Journal/Newspaper Beluga Beluga* DataCite Metadata Store (German National Library of Science and Technology) |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
unknown |
topic |
Programming Languages cs.PL FOS Computer and information sciences |
spellingShingle |
Programming Languages cs.PL FOS Computer and information sciences Sano, Chuta Kavanagh, Ryan Pientka, Brigitte Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
topic_facet |
Programming Languages cs.PL FOS Computer and information sciences |
description |
Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as ... : Technical report containing an appendix with additional proofs. Companion to an OOPSLA'23 paper of the same name ... |
format |
Article in Journal/Newspaper |
author |
Sano, Chuta Kavanagh, Ryan Pientka, Brigitte |
author_facet |
Sano, Chuta Kavanagh, Ryan Pientka, Brigitte |
author_sort |
Sano, Chuta |
title |
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
title_short |
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
title_full |
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
title_fullStr |
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
title_full_unstemmed |
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity ... |
title_sort |
mechanizing session-types using a structural view: enforcing linearity without linearity ... |
publisher |
arXiv |
publishDate |
2023 |
url |
https://dx.doi.org/10.48550/arxiv.2309.12466 https://arxiv.org/abs/2309.12466 |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_rights |
Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 |
op_doi |
https://doi.org/10.48550/arxiv.2309.12466 |
_version_ |
1781697079797612544 |