Tracing sharing in an imperative pure calculus
- We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize, widely-used notions in literature, notably uniqueness and borrowing. Moreover, the calculus is pure in the sense that reduction is defined on language terms only, since they directly encode store. The advantage of this non-standard execution model with respect to a behaviorally equivalent standard model using a global auxiliary structure is that reachability relations among references are partly encoded by scoping. (C) 2018 Elsevier B.V. All rights reserved.
| Author details: | Paola Giannini, Tim Richter, Marco Servetto, Elena ZuccaORCiD |
|---|---|
| DOI: | https://doi.org/10.1016/j.scico.2018.11.007 |
| ISSN: | 0167-6423 |
| ISSN: | 1872-7964 |
| Title of parent work (English): | Science of computer programming |
| Publisher: | Elsevier |
| Place of publishing: | Amsterdam |
| Publication type: | Article |
| Language: | English |
| Date of first publication: | 2018/12/03 |
| Publication year: | 2018 |
| Release date: | 2021/03/31 |
| Tag: | Imperative calculi; Sharing; Type and effect systems |
| Volume: | 172 |
| Number of pages: | 23 |
| First page: | 180 |
| Last Page: | 202 |
| Funding institution: | Universita del Piemonte Orientate |
| Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
| DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
| Peer review: | Referiert |
