|
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
|