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...
Published in: | Proceedings of the ACM on Programming Languages |
---|---|
Main Authors: | , , |
Other Authors: | , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2023
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1145/3622810 https://dl.acm.org/doi/pdf/10.1145/3622810 |
id |
cracm:10.1145/3622810 |
---|---|
record_format |
openpolar |
spelling |
cracm:10.1145/3622810 2024-09-15T17:59:01+00:00 Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity Sano, Chuta Kavanagh, Ryan Pientka, Brigitte Natural Sciences and Engineering Research Council of Canada Fonds de recherche du Québec - Nature et Technologies 2023 http://dx.doi.org/10.1145/3622810 https://dl.acm.org/doi/pdf/10.1145/3622810 en eng Association for Computing Machinery (ACM) Proceedings of the ACM on Programming Languages volume 7, issue OOPSLA2, page 374-399 ISSN 2475-1421 journal-article 2023 cracm https://doi.org/10.1145/3622810 2024-07-15T04:02:56Z 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 session-typed languages. Article in Journal/Newspaper Beluga Beluga* ACM Publications (Association for Computing Machinery) Proceedings of the ACM on Programming Languages 7 OOPSLA2 374 399 |
institution |
Open Polar |
collection |
ACM Publications (Association for Computing Machinery) |
op_collection_id |
cracm |
language |
English |
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 session-typed languages. |
author2 |
Natural Sciences and Engineering Research Council of Canada Fonds de recherche du Québec - Nature et Technologies |
format |
Article in Journal/Newspaper |
author |
Sano, Chuta Kavanagh, Ryan Pientka, Brigitte |
spellingShingle |
Sano, Chuta Kavanagh, Ryan Pientka, Brigitte Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity |
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 |
Association for Computing Machinery (ACM) |
publishDate |
2023 |
url |
http://dx.doi.org/10.1145/3622810 https://dl.acm.org/doi/pdf/10.1145/3622810 |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
Proceedings of the ACM on Programming Languages volume 7, issue OOPSLA2, page 374-399 ISSN 2475-1421 |
op_doi |
https://doi.org/10.1145/3622810 |
container_title |
Proceedings of the ACM on Programming Languages |
container_volume |
7 |
container_issue |
OOPSLA2 |
container_start_page |
374 |
op_container_end_page |
399 |
_version_ |
1810435976468627456 |