Efficient type-checking for amortised heap-space analysis

Abstract

The prediction of resource consumption in programs has gained interest in the last years. It is important for a number of areas, notably embedded systems and safety critical systems. Different approaches to achieve bounded resource consumption have been analysed. One of them, based on an amortised complexity analysis, has been studied by Hofmann and Jost in 2006 for a Java-like language. In this paper we present an extension of this type system consisting of more general subtyping and sharing relations that allows us to type more examples. Moreover we describe efficient automated type-checking for a finite, annotated version of the system. We prove soundness and completeness of the type checking algorithm and show its efficiency. © 2009 Springer Berlin Heidelberg.