{"ID":2865668,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.22982","arxiv_id":"2509.22982","title":"Efficient Cost Bounds with Linear Maps","abstract":"The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring cost-free types using the current state-of-the-art algorithm is expensive due to recursive dependence on additional cost-free types. Furthermore, that algorithm uses a heuristic only applicable to polynomial cost bounds, and not, e.g., exponential bounds. This paper presents a new approach to these problems by representing the cost-free types of a function in a new way: with a linear map, which can stand for infinitely many cost-free types. Such maps enable an algebraic flavor of reasoning about cost bounds (including non-polynomial bounds) via matrix inequalities. These inequalities can be solved with off-the-shelf linear-programming tools for many programs, so that types can always be efficiently checked and often be efficiently inferred. An experimental evaluation with a prototype implementation shows that-when it is applicable-the inference of linear maps is exponentially more efficient than the state-of-the-art algorithm.","short_abstract":"The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring cost-free types using the current state-of-the-art algorithm is expensive due to recu...","url_abs":"https://arxiv.org/abs/2509.22982","url_pdf":"https://arxiv.org/pdf/2509.22982v1","authors":"[\"David M Kahn\",\"Jan Hoffmann\",\"Thomas Reps\",\"Jessie Grosen\"]","published":"2025-09-26T22:29:42Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}