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

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

Acknowledgments

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