Staged Notational Definitions

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Appalachian State University (ASU )
Web Site:

Abstract: Recent work proposed defining type-safe macros via interpretation into a multi-stage language. The utility of this approach was illustrated with a language called MacroML, in which all type checking is carried out before macro expansion. Building on this work, the goal of this paper is to develop a macro language that makes it easy for programmers to reason about terms locally. We show that defining the semantics of macros in this manner helps in developing and verifying not only type systems for macro languages but also equational reasoning principles. Because the MacroML calculus is sensitive to renaming of (what appear locally to be) bound variables, we present a calculus of staged notational definitions (SND) that eliminates the renaming problem but retains MacroML’s phase distinction. Additionally, SND incorporates the generality of Griffin’s account of notational definitions. We exhibit a formal equational theory for SND and prove its soundness.

Additional Information

Taha, W. and Johann, P. (2003). Staged Notational Definitions. Proceedings, Generative Programming and Component Engineering 2003 (GPCE '03), pp. 97-116. NC Docks permission to re-print granted by author(s).
Language: English
Date: 2003
MacroML, semantics of macros, staged notational definitions (SND), programming, renaming

Email this document to