| Sommario: | In this paper we introduce a type and effect system, for an
imperative object calculus, which infers sharing possibly introduced by
the evaluation of an expression. Sharing is directly represented at the
syntactic level as a relation among free variables, thanks to the fact
that the calculus is pure. That is, imperative features are modeled by
just rewriting source code terms. We consider both standard variables
and affine variables, which can occur at most once in their scope. The
latter are used as temporary references, to “move” a capsule (an isolated
portion of store) to another location in the store. The sharing effects
inferred by the type system are very expressive, and generalize notions
introduced in literature by type modifiers. |
