Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2022.23
URN: urn:nbn:de:0030-drops-162518
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16251/
Jacobs, Jules
A Self-Dual Distillation of Session Types
| pdf-format: |
|
Abstract
We introduce ƛ ("lambda-barrier"), a minimal extension of linear λ-calculus with concurrent communication, which adds only a single new fork construct for spawning threads. It is inspired by GV, a session-typed functional language also based on linear λ-calculus. Unlike GV, ƛ strives to be as simple as possible, and adds no new operations other than fork, no new type formers, and no explicit definition of session type duality. Instead, we use linear function function type τ₁ -∘ τ₂ for communication between threads, which is dual to τ₂ -∘ τ₁, i.e., the function type constructor is dual to itself. Nevertheless, we can encode session types as ƛ types, GV’s channel operations as ƛ terms, and show that this encoding is type-preserving. The linear type system of ƛ ensures that all programs are deadlock-free and satisfy global progress, which we prove in Coq. Because of ƛ’s minimality, these proofs are simpler than mechanized proofs of deadlock freedom for GV.
BibTeX - Entry
@InProceedings{jacobs:LIPIcs.ECOOP.2022.23,
author = {Jacobs, Jules},
title = {{A Self-Dual Distillation of Session Types}},
booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)},
pages = {23:1--23:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-225-9},
ISSN = {1868-8969},
year = {2022},
volume = {222},
editor = {Ali, Karim and Vitek, Jan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16251},
URN = {urn:nbn:de:0030-drops-162518},
doi = {10.4230/LIPIcs.ECOOP.2022.23},
annote = {Keywords: Linear types, concurrency, lambda calculus, session types}
}
| Keywords: | Linear types, concurrency, lambda calculus, session types | |
| Seminar: | 36th European Conference on Object-Oriented Programming (ECOOP 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 23.06.2022 | |
| Supplementary Material: |
Software (ECOOP 2022 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.8.2.15 Software (Mechanized proofs): https://zenodo.org/record/6560443 |
