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.

Tracing sharing in an imperative pure calculus (extended abstract)

Giannini, Paola;Zucca, Elena
2017-01-01

Abstract

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.
2017
9781450350983
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/887199
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact