Tracing sharing in an imperative pure calculus
Autor: | Marco Servetto, Elena Zucca, Paola Giannini, Tim Richter |
---|---|
Rok vydání: | 2019 |
Předmět: |
Computer science
Institut für Informatik und Computational Science Imperative calculi Sharing Type and effect systems Effect system 020207 software engineering 02 engineering and technology Object (computer science) Expression (mathematics) Reachability 020204 information systems Free variables and bound variables 0202 electrical engineering electronic engineering information engineering Calculus Equivalence relation ddc:004 Direct representation Execution model Software |
Zdroj: | Science of Computer Programming. 172:180-202 |
ISSN: | 0167-6423 |
DOI: | 10.1016/j.scico.2018.11.007 |
Popis: | 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. |
Databáze: | OpenAIRE |
Externí odkaz: |