Publications:Staged Notational Definitions

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Staged Notational Definitions
Author Walid Taha and Patricia Johann
Year 2003
PublicationType Conference Paper
Conference GPCE'03 International Conference on Generative Programming and Component Engineering.
Diva url
Abstract Recent work proposed defining type-safe macros via interpretation into a multi-stage language. The utility of this approach wasillustrated with a language called MacroML, in which all type checking is carried out before macro expansion. Building on this work, thegoal of this paper is to develop a macro language that makes it easy forprogrammers to reason about terms locally. We show that defining thesemantics of macros in this manner helps in developing and verifyingnot only type systems for macro languages but also equational reasoning principles. Because the MacroML calculus is sensetive to renamingof (what appear locally to be) bound variables, we present a calculus ofstaged 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. Weexhibit a formal equational theory for SND and prove its soundness.