http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM11Rhiger 2026-04-05T20:56:52Z Revision history for this page on the wiki MediaWiki 1.43.5 http://mw.hh.se/wg211/index.php?title=WG211/M11Rhiger&diff=652&oldid=prev 2012-06-03T20:00:02Z

<p>Created page with &quot;&#039;&#039;&#039;A lexically scoped type system for multi-stage languages&#039;&#039;&#039; by Morten Rhiger Static type systems for multi-stage programming languages must guarantee that well-typed programs...&quot;</p> <p><b>New page</b></p><div>&#039;&#039;&#039;A lexically scoped type system for multi-stage languages&#039;&#039;&#039; by Morten Rhiger<br /> <br /> Static type systems for multi-stage programming languages must<br /> guarantee that well-typed programs only generate, combine, and<br /> execute code values that are themselves well typed.<br /> <br /> We present &quot;lambda open box&quot;, a simple core type system for a<br /> statically typed, hygienic, multi-stage lambda-calculus that<br /> supports evaluation under future-stage binders, open-code<br /> manipulation, a first-class eval function, and mutable state. The<br /> type system provides one type of lexically scoped code that<br /> precisely accounts for the contexts in which code values can be<br /> inserted. This type system demonstrates that alpha-equivalence<br /> is compatible with code types that carry type environments.<br /> <br /> We then outline a general polymorphic extension to lambda open<br /> box that provides a significant increase in expressiveness. We<br /> compare the resulting polymorphic type system to existing<br /> multi-stage calculi.</div>

Ups