Automatic amortized resource analysis (AARA) is a type-based technique for inferring symbolic resource bounds for programs at compile time. Since its first introduction, the technique has been extended to the analysis to different resource metrics, evaluation strategies, non-linear bounds, and various language features.

This thesis builds upon AARA. The contribution consists of two parts. First, we present a new soundness proof of the type system of AARA with respect to a small-step, operational cost semantics on an abstract machine that makes control flow explicit. Compared to the big-step, structural cost semantics adopted in the previous works, it leads to a more concise type soundness proof that is amenable to extension to complex language features, such as polymorphism and nonstandard control flows. Second, we extend the technique of AARA to a language with ex- ception handling in the style of Standard ML. We present a type system, prove its soundness by extending the small-step soundness proof, and show resource safety as a corollary of the type soundness theorem. We discuss how type inference can be automated to achieve, for the first time, automatic amortized resource analysis for programs with exception handling.

41 pages

Thesis Committee:
Jan Hoffman (Chair)
Robert Harper

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu