Functional Programming and Resource Bounds

Dr Kenneth MacKenzie, University of Edinburgh

In recent years there has been considerable interest in the static prediction of resource usage (in particular, heap-space usage) for functional programs.

The Camelot language has been developed as part of the Mobile Resource Guarantees (MRG) project at Edinburgh, where it is used in a proof-carrying code framework which equips mobile programs with checkable guarantees of memory usage. We will give a brief overview of the MRG framework and then describe Camelot, which is a functional language with features which allow explicit manipulation of memory cells. We will also describe some type-theoretic techniques which can be used to prove that memory is manipulated in a safe manner, and to infer provable bounds for the heap-space usage of programs.