A type-theoretic interpretation of pointcuts and advice

Jay Ligatti, David Walker, Steve Zdancewic

Research output: Contribution to journalArticlepeer-review

14 Scopus citations


This article defines the semantics of MinAML, an idealized aspect-oriented programming language, by giving a type-directed translation from a user-friendly external language to a compact, well-defined core language. We argue that our framework is an effective way to give semantics to aspect-oriented programming languages in general because the translation eliminates shallow syntactic differences between related constructs and permits definition of an elegant and extensible core language. The core language extends the simply-typed lambda calculus with two central new abstractions: explicitly labeled program points and first-class advice. The labels serve both to trigger advice and to mark continuations that the advice may return to. These constructs are defined orthogonally to the other features of the language and we show that our abstractions can be used in both functional and object-oriented contexts. We prove Preservation and Progress lemmas for our core language and show that the translation from MinAML source into core is type-preserving. Together these two results imply that the source language is type safe. We also consider several extensions to our basic framework including a general mechanism for analyzing the current call stack.

Original languageEnglish (US)
Pages (from-to)240-266
Number of pages27
JournalScience of Computer Programming
Issue number3
StatePublished - Dec 15 2006

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Computational Theory and Mathematics
  • Modeling and Simulation


  • Aspect-oriented programming languages
  • Aspects
  • Operational semantics
  • Type theory


Dive into the research topics of 'A type-theoretic interpretation of pointcuts and advice'. Together they form a unique fingerprint.

Cite this