Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916648391278592 |
|---|---|
| author | Bagrel, Thomas Spiwack, Arnaud |
| author_facet | Bagrel, Thomas Spiwack, Arnaud |
| contents | Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_07489 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes Bagrel, Thomas Spiwack, Arnaud Programming Languages Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant. |
| title | Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2503.07489 |