Title
Tracing sharing in an imperative pure calculus.
Abstract
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.
Year
DOI
Venue
2018
10.1016/j.scico.2018.11.007
Science of Computer Programming
Keywords
Field
DocType
Imperative calculi,Sharing,Type and effect systems
Uniqueness,Equivalence relation,Effect system,Computer science,Direct representation,Free variables and bound variables,Theoretical computer science,Reachability,Execution model,Syntax,Calculus
Journal
Volume
ISSN
Citations 
172
0167-6423
0
PageRank 
References 
Authors
0.34
22
4
Name
Order
Citations
PageRank
Paola Giannini144950.00
Tim Richter200.34
Marco Servetto36111.51
Elena Zucca4497101.25