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