Computer Science 5th Years Master's Thesis Presentation
— 11:00am
Location:
In Person and Remote - ET
-
Gates Hillman 7101and Zoom
Speaker:
YIYANG GUO
,
Master's Student, Computer Science Department, Carnegie Mellon Universit
Automatic Amortized Resource Analysis for Exception Handling
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 exception 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.
Thesis Committee:
Jan Hoffmann (Chair)Robert Harper
Additional Information
In Person and Zoom Participation. See announcement.