Vineet Rajani

A unifying type-theory for higher-order (amortized) cost analysis

2021 · Proceedings of the ACM on Programming Languages

This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. λ-amor introduces a new modal …