Abstract
|
<p>Recent work proposed defining type … <p>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.</p>for SND and prove its soundness.</p>
|
Author
|
Walid Taha +
, Patricia Johann +
|
Conference
|
GPCE'03 International Conference on Generative Programming and Component Engineering.
|
Diva
|
http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588277
|
PublicationType
|
Conference Paper +
|
Title
|
Staged Notational Definitions +
|
Year
|
2003 +
|
Has queryThis property is a special property in this wiki.
|
Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
, Publications:Staged Notational Definitions +
|
Categories |
Publication +
|
Modification dateThis property is a special property in this wiki.
|
26 June 2014 03:45:11 +
|