Copenhagen Programming Language Seminar
In a joint work with Martin Hofmann, which appeared in the proceedings of POPL'03, we show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs.
The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection.
The analysis relies on a type system with resource annotations. These resource annotations may be inferred automatically using standard Linear Programming (LP) which is known to be feasible both in theory and practice. A functions annotated type then immediately yields a linear arithmetic expression which describes its heap space consumption in terms of the size of the functions input/output.
While non-linearly typed programs containing types with rational annotations are acceptable, it is shown that, due to an earlier work, a particular integer solution to the LP of a linearly typed program allows evaluation without any operating system support for memory management.
Although the obtained bounds are linear, we already cover a wide variety of examples including, for instance, the familiar sorting algorithms for lists (insertion-, quick- & heapsort).
We will obtain an understanding of the works approach and we will study some illustrative examples using the recently finished implementation of our type inference.
Martin Elsman. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to firstname.lastname@example.org with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org