The Fox Project
Staged Computation

Contents Recent Talks | Recent Publications | Software | Collaborations | Further Links
Elsewhere Bibliography

Staged computation refers to explicit or implicit division of a task into stages. It is a standard technique from algorithm design that has found its way to programming languages and environments. Examples are partial evaluation which refers to the global specialization of a program based on a division of the input into static (early) and dynamic (late) data, and run-time code generation which refers to the dynamic generation of optimized code based on run-time values of inputs.

The technology of staged computation is developed in the Fox project in order to allow the modular and safe construction of programs without sacrificing efficiency. Our emphasis has been on lightweight run-time code generation and its logical foundations. Our approach is to make staging explicit in the language (rather than leave it implicit in a tool) and to verify proper staging statically (rather than dynamically or not at all).

Overview references:

Recent Talks

Safe Explicitly Staged Computation
Frank Pfenning.
DARPA PCES PI Meeting, San Diego California, February 2001.
Slides (PowerPoint, HTML)
Reasoning About Staged Computation
Frank Pfenning.
Invited talk at the Workshop on Semantics, Applications and Implementation of Program Generation (SAIG'00) Montreal, Canada, September 2000.
Abstract, Slides.
On the Logical Foundations of Staged Computation
Frank Pfenning.
Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00), Boston, Massachusetts, January 2000. Invited talk.
Abstract (Text, PostScript), Slides (PostScript, PDF).

Recent Publications

Below are some recent papers related to staged computation in the Fox project. A more complete bibliography is also available.

A Modal Analysis of Staged Computation
Rowan Davies and Frank Pfenning.
Journal of the ACM. To appear. Significantly extended and revised version of a technical summary from POPL'96.
A Judgmental Reconstruction of Modal Logic
Frank Pfenning and Rowan Davies.
Mathematical Structures in Computer Science. To appear. Notes for an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999.


Our software for staged computation is still under development and has not yet been released.


We are collaborating with the Cornell project on Typed Assembly Language which includes work on the Cyclone compiler for run-time code generation

Further Links

[ Home | Contact Information | Publications | Researchers ]
[ FoxNet | Typed Intermediate Languages | Proof-Carrying Code ]
[ Logical Frameworks | Staged Computation | Language Design ]