Lambda the Ultimate

inactiveTopic Selective Memoization
started 3/14/2003; 4:46:54 AM - last post 3/14/2003; 4:46:54 AM
Ehud Lamm - Selective Memoization  blueArrow
3/14/2003; 4:46:54 AM (reads: 2114, responses: 0)
Selective Memoization
Umut Acar, Guy Blelloch, and Robert Harper. Selective Memoization. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, LA, January, 2003.

We present a framework for applying memoization selectively. The framework provides programmer control over equality, space usage, and identification of precise dependences so that memoization can be applied according to the needs of an application. Two key properties of the framework are that it is efficient and yields programs whose performance can be analyzed using standard techniques.

We describe the framework in the context of a functional language and an implementation as an SML library. The language is based on a modal type system and allows the programmer to express programs that reveal their true data dependences when executed. The SML implementation cannot support this modal type system statically, but instead employs run-time checks to ensure correct usage of primitives.

The authors present a small functional language, called MFL, that supports selective memoization. MFL is equipped with a modality for tracking dependences on data structures within memoized code.

The paper proves a soundness theorem stating that memoization does not affect the outcome of a computation compared to a standard, non-memoizing semantics.

Section 2, Background and Related Work, is a nice overview of the design pressures in implementing memoization.


Posted to functional by Ehud Lamm on 3/14/03; 4:53:46 AM