TFP'08 paper

Prediction of linear memory usage for first-order functional programs

In Preproceedings of The Ninth Symposium on Trends in Functional Programming (TFP), 2008.

Hofmann and Jost have presented a type inference system for a pure first-order functional language which uses linear programming to give linear upper bounds on heap memory usage with respect to the input size. We present an extended analysis which infers bounds for heap and stack space requirements, and which uses more expressive post-evaluation bounds to model a common pattern of stack space use.

The paper is available here as a PDF document, as well as the slides from the talk. There is also an implementation of the inference, based on Steffen Jost's lfd_infer. It requires ocaml and GNU make to build it, and lpsolve to solve the resulting linear programs. (It has only been tested on Linux, however.) See the README.TXT file for more information about building it and running the inference on the included examples.