Finding resource bounds in the presence of explicit deallocation

Abstract. A software program requesting a resource that is not avail-able usually raises an out-of-resource exception. Component software is software that has been assembled from standardized, reusable compo-nents which, in turn, may also composed from other components. Due to the independent development and reuse of components, component soft-ware has a high risk of causing out-of-resource exceptions. We present a small component language and develop a type system which can stati-cally prevent this type of errors. This work continues our previous works [3, 18] by including explicit deal-location. We prove that the type system is sound with respect to safe deallocation and that sharp resource bounds can be computed statically.