Research on "Formal Methods in Computing"

Alias types for ``environment-aware'' computations

Work partially supported by IST-2001-33477 DART, MURST Cofin '01 NAPOLI, and MURST Cofi'02 McTati projects.

ABSTRACT. In previous work we introduced a calculus for modelling ``environment-aware'' computations, that is computations that adapt their behavior according to the capabilities of the environment. The calculus is an imperative, object-based language (with extensible objects and primitives for discriminating the presence or absence of attributes of objects) equipped with a small-step operational semantics.
In this paper we define a type and effect system for the calculus. The typing judgements specify, via constraints, the shape of environments which guarantees the correct execution of expressions and the typing rules track the effect of expression evaluation on the environment. The type and effect system is sound w.r.t. the operational semantics of the language.

• ps , pdf

BIBTEX.

@inproceedings{Damiani-Giannini:WOOD-03,
   author    = {F. Damiani and P. Giannini},
   title     = {{Alias types for ``environment-aware'' computations}},
   booktitle = {WOOD'03},
   year      = {2003},
   publisher = {Elsevier},
   series    = {ENTCS},
   volume    = {82.8}
}