A typed calculus for aspect-oriented programs. Submitted for publication, at http://fpl.cs.depaul.edu/ajeffrey/papers/typedABL. pdf

Abstract. Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. In earlier work, we described an untyped calculus of aspect programs with a direct description of the dynamic semantics. This calculus provides a specification for the correctness of weaving. In this paper, we turn our attention to the interaction of aspects and types, whose subtleties are amply illustrated by the difficulties encountered by current compilers of aspect languages. We develop a typed calculus of aspect programs that includes inner classes, concurrency and dynamic arrival of new advice. To our knowledge, this is the first source-level typing system for a class-based aspectoriented language. We prove that types are preserved by reduction in the aspect calculus and that well-typed programs make progress. We also show that weaving preserves typability of programs by mapping well-typed aspect programs to well-typed class based programs.