A modal analysis of staged computation

DOI Web Site 11 Citations

Search this article

Description

<jats:p> We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed λ-calculi and functional languages. We directly demonstrate the sense in which our λ <jats:sub>e</jats:sub> <jats:sup>→□</jats:sup> -calculus captures staging, and also give a conservative embeddng of Nielson and Nielson's two-level functional language in our functional language Mini-ML <jats:sup>□</jats:sup> , thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition, Mini-ML <jats:sup>□</jats:sup> can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation. </jats:p>

Journal

  • Journal of the ACM

    Journal of the ACM 48 (3), 555-604, 2001-05

    Association for Computing Machinery (ACM)

Citations (11)*help

See more

Details 詳細情報について

Report a problem

Back to top