Welcome to the Rice PLT homepage of

Multi-stage Programming (MSP)

Type-safe program generation.

Introduction

In addition to having the usual constructs of a general-purpose language, multi-stage languages internalize the notions of runtime program generation and execution. Thus, multi-stage languages provide the programmer with the essence of partial evaluation and program specialization techniques, both of which have been shown to lead to dramatic resource-utilization gains in a wide range of applications, starting from implementations of domain-specific compilers, to high-performance operating systems. Multi-stage languages make it possible to write generic and highly-parameterized programs that do not pay unnecessary runtime overheads.

Checkout MetaOCaml, our implementation of multi-stage programming based on OCaml.

Multi-Stage Programming Papers

Introductions

• Multi-stage programming with explicit annotations, PEPM'97 (a longer version appears in TCS'00.)
• Multi-stage programming:  Its theory and its applications (Th'99)

Implementation

• (in preperation)

Applications

• Macros as multi-stage computations (ICFP'01)

Semantics and Type Systems

• Idealized MetaML: Simpler, and more expressive (ESOP'99)
• Logical modalities and multi-stage programming (IMLA'99)
• Sound reductions for untyped CBN MetaML (PEPM'00)
• Closed types as a simple approach to safe imperative multi-stage programming (ICALP'00)
• Closed Types for a Safe Imperative MetaML (JFP)

Tag Elimination

• Tag elimination - or - type specialization is a type-indexed effect (DTP'00)
• Tag elimination and Jones-optimality (PADO II)

These papers are also available in dvi and ps formats.

The MSP Team

Walid Taha

Cristiano Calcagno

Liwen Huang

Xavier Leroy

Acknowledgments

This work was funded by NSF ITR on "Putting Multi-stage Annotations to Work"