Central Idea

They propose a type system for verifying that programs correctly implement constant-resource behaviour, using Automatic Amortised Resource Analysis (AARA)

Automatic Amortised Resource Analysis