CMU-CS-99-153
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-99-153

A Modal Analysis of Staged Computation

Rowan Davies, Frank Pfenning

August 1999

Also appears as FOX Memorandum CMU-FOX-TR-99-02

CMU-CS-99-153.ps
CMU-CS-99-153.pdf


Keywords: Programming languages, staged computation, modal logic


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 lambda-calculi and functional languages. We directly demonstrate the sense in which our calculus captures staging, and also give a conservative embedding of Nielson & Nielson's two-level functional language in our language, thus proving that binding-time correctness is equivalent to modal correctness. In addition, our language can express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.

53 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu