Weak-linearity, globality and in-place update
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910572682936320 |
|---|---|
| author | Gramaglia, Hector |
| author_facet | Gramaglia, Hector |
| contents | Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle. This has promoted numerous investigations into safe introduction of in-place update. Various type systems have been proposed for this aim, but the memory management that promotes linear evaluation does not adequately model the destruction of in-place update. The main achievement of this work is to establish a simple theoretical framework that will allow us to clarify the potential (and limits) of linearity to guarantee the process of transforming a functional program into an imperative one. For this purpose we will introduce a type system called "global" that will model the in-place update as the linear system models the one-time use. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_16534 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Weak-linearity, globality and in-place update Gramaglia, Hector Programming Languages D.2.4; D.3.3; F.3.3; F.3.1 Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle. This has promoted numerous investigations into safe introduction of in-place update. Various type systems have been proposed for this aim, but the memory management that promotes linear evaluation does not adequately model the destruction of in-place update. The main achievement of this work is to establish a simple theoretical framework that will allow us to clarify the potential (and limits) of linearity to guarantee the process of transforming a functional program into an imperative one. For this purpose we will introduce a type system called "global" that will model the in-place update as the linear system models the one-time use. |
| title | Weak-linearity, globality and in-place update |
| topic | Programming Languages D.2.4; D.3.3; F.3.3; F.3.1 |
| url | https://arxiv.org/abs/2402.16534 |