The Fox Project
Staged Computation

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:

• Dynamic Specialization in the Fabius System (Computing Surveys) [Leone and Lee 1998]
• Modal Types as Staging Sepcifications for Run-time Code Generation (Computing Surveys) [Wickline et al. 1998
• Optimizing ML with Run-Time Code Generation (PLDI'96) [Lee and Leone 96]
• A Modal Analysis of Staged Computation (JACM, to appear) [Davies and Pfenning 2000]

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.

Software

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

Collaborations

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

• Overview of Partial Evaluation
• Special issue of Computing Surveys on Partial Evaluation
• Tempo home page
• MetaML home page

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

Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/