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 type for representing potentials – costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, λ-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. λ-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in λ-amor showing that, despite its simplicity, λ-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that λ-amor is relatively complete for all terminating PCF programs.

@article{paperbot1202,
  title = {A unifying type-theory for higher-order (amortized) cost analysis},
  author = {Vineet Rajani and Marco Gaboardi and Deepak Garg and Jan Hoffmann},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434308}
}