Browse wiki

From CERES
Jump to: navigation, search
Publications:Tagless Staged Interpreters for Typed Languages
Abstract <p>Multi-stage programming languages<p>Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving animplementation that is both readable and efficient. In an untypedsetting, staging an interpreter “removes a complete layer of interpretive overhead”, just like partial evaluation. In a typed settinghowever, Hindley-Milner type systems do not allow us to exploittyping information in the language being interpreted. In practice,this can mean a slowdown cost by a factor of three or more.Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experiencewith the issues that arise in writing such an interpreter and in designing such a language.To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (calledMeta-D) and prove its type safety. To formalize Meta-D, we extendShao, Saha, Trifonov and Papaspyrou’s λH language to a multilevel setting. Building on λH allows us to demonstrate type safetyin a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work neededfor establishing the soundness of that system.</p>ng the soundness of that system.</p>
Author Emir Pasalic + , Walid Taha + , Tim Sheard +
Conference ICFP'02. International Conference on Functional Programming
Diva http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588280
PublicationType Conference Paper  +
Title Tagless Staged Interpreters for Typed Languages  +
Year 2002  +
Has queryThis property is a special property in this wiki. Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages + , Publications:Tagless Staged Interpreters for Typed Languages +
Categories Publication  +
Modification dateThis property is a special property in this wiki. 26 June 2014 03:44:58  +
hide properties that link here 
  No properties link to this page.
 

 

Enter the name of the page to start browsing from.