2003/01/15 by Martin Hofmann, Martin R. Hofmann, Steffen Jost
Computer Science · #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Security and Verification in Computing
paper · doi:10.1145/640128.604148
openalex publication_date 2003/01/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/25
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. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort.The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system.We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.