Carnegie Mellon University
file.pdf (392.38 kB)

A Modal Analysis of Staged Computation

Download (392.38 kB)
journal contribution
posted on 1976-01-01, 00:00 authored by Rowan Davies, Frank Pfenning
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 λe-calculus captures staging, and also give a conservative embeddng of Nielson and Nielson's two-level functional language in our functional language Mini-ML , thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition, Mini-ML; can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.


Publisher Statement

All Rights Reserved



Usage metrics