Università di Torino

Research on "Formal Methods in Computing"

Alias types for ``environment-aware'' computations

Ferruccio DAMIANI and Paola GIANNINI

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.


   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}

["Formal Methods in Computing" group] [Department's HOME]

Last update: Apr 27, 2004