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.