@inbook {IOPORT.06049283, author = {Rhiger, Morten}, title = {Staged computation with staged lexical scope.}, year = {2012}, booktitle = {Programming languages and systems. 21st European symposium on programming, ESOP 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24--April 1, 2012. Proceedings}, isbn = {978-3-642-28868-5}, pages = {559-578}, publisher = {Berlin: Springer}, doi = {10.1007/978-3-642-28869-2_28}, abstract = {Summary: We present a simple core type system, $\lambda ^{[ ]}$ - pronounced ``lambda open box'' - for a statically typed, hygienic, and multi-stage lambda-calculus supporting evaluation under future-stage binders, open-code manipulation, a first-class eval function, and mutable state. The type system provides one type of lexically scoped code that precisely accounts for the contexts in which code values can be inserted. In particular, this type can distinguish between open and closed code. We show how to extend $\lambda ^{[ ]}$ with subtype polymorphism over program contexts. The soundness and simplicity of $\lambda ^{[ ]}$ demonstrate that the notion of staging is orthogonal to features that have been presented as instrumental in existing type systems for staged computation, such as polymorphism, nameless term representations, explicit substitutions, and delimited continuations.}, identifier = {06049283}, }