A Modal Analysis of Staged Computation
Abstract
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 and 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1999
- Accession Number
- ADA367677
Entities
People
- Frank Pfenning
- Rowan Davies
Organizations
- Carnegie Mellon University