Title: Amortised Upper Bound Cost Analysis for Hume

Kevin Hammond


Abstract

This talk introduces a generic approach for determining upper bounds costs on 
time, stack and heap metrics for the strict purely functional language, Hume. 
We construct cost models that are correlated to a formal operational semantics 
for Hume programs.  These cost models are used to derive a type system that 
exposes explicit input/output constraints on the cost metrics of interest, and 
which can be solved using standard solver technology.  By using an amortised 
analysis, where we track the potential usage and destruction of each value,  we 
are able to obtain linear cost bounds in several interesting cases.  The talk 
introduces the Hume language, describes the approach, and provides examples.