journal article
Apr 10, 2026
Handling Exceptions and Effects with Automatic Resource Analysis
Proceedings of the ACM on Programming Languages
Vol. 10
No. OOPSLA1
pp. 201-230
·
Association for Computing Machinery (ACM)
Abstract
There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large class of programs and language features. However, non-local transfer of control as needed for exception or effect handlers has remained a challenge.
This paper presents the first automatic resource bound analysis that supports non-local control transfer between exceptions or effects and their handlers. The analysis is an extension of type-based automatic amortized resource analysis (AARA), which automates the potential method of amortized analysis. It is presented for a simple functional language with lists and linear potential functions. However, the ideas are directly applicable to richer settings and implemented for Standard ML and polynomial potential functions.
Apart from the new type system for exceptions and effects, a main contribution is a novel syntactic type- soundness theorem that establishes the correctness of the derived bounds with respect to a stack-based abstract machine. An experimental evaluation shows that the new analysis is capable of analyzing programs that cannot be analyzed by existing methods and that the efficiency overhead of supporting exception and effect handlers is low.
This paper presents the first automatic resource bound analysis that supports non-local control transfer between exceptions or effects and their handlers. The analysis is an extension of type-based automatic amortized resource analysis (AARA), which automates the potential method of amortized analysis. It is presented for a simple functional language with lists and linear potential functions. However, the ideas are directly applicable to richer settings and implemented for Standard ML and polynomial potential functions.
Apart from the new type system for exceptions and effects, a main contribution is a novel syntactic type- soundness theorem that establishes the correctness of the derived bounds with respect to a stack-based abstract machine. An experimental evaluation shows that the new analysis is capable of analyzing programs that cannot be analyzed by existing methods and that the efficiency overhead of supporting exception and effect handlers is low.
Topics
No keywords indexed for this article. Browse by subject →
References
110
[2]
Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In 15th Static Analysis Symp. (SAS’08). 221–237.
[3]
Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, 161–203.
10.1007/s10817-010-9174-1
[4]
Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. 2007. Cost Analysis of Java Bytecode. In 16th Euro. Symp. on Prog. (ESOP’07).
[7]
Elvira Albert, Jesús Correas Fernández, and Guillermo Román-Díez. 2015. Non-cumulative Resource Analysis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, (TACAS’15).
[8]
Elvira Albert, Samir Genaim, and Abu Naser Masud. 2013. On the Inference of Resource Usage Upper and Lower Bounds. ACM Transactions on Computational Logic, 14, 3 (2013).
[9]
Robert Atkey. 2010. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP’10).
[10]
[11]
Martin Avanzini, Ugo Dal Lago, and Georg Moser. 2012. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th Int. Conf. on Functional Programming (ICFP’15).
[12]
Martin Avanzini and Georg Moser. 2013. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA’13).
[13]
[14]
[16]
Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovács. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR’10).
[17]
Guy E. Blelloch. 1995. NESL: A Nested Data-Parallel Language (Version 3.1). CMU.
[18]
Guy E. Blelloch and John Greiner. 1996. A Provable Time and Space Efficient Implementation of NESL. In 1st Int. Conf. on Funct. Prog. (ICFP’96).
[19]
Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In 20th Int. Conf. on Tools and Alg. for the Constr. and Anal. of Systems (TACAS’14).
[23]
Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2017. Non-polynomial Worst-Case Analysis of Recursive Programs. In Computer Aided Verification - 29th Int. Conf. (CAV’17).
[24]
[25]
Ethan Chu. 2023. The Theory and Implementation of Resource Aware ML 2. Master’s thesis. Carnegie Mellon University. http://reports-archive.adm.cs.cmu.edu/anon/2023/CMU-CS-23-140.pdf
[26]
Ethan Chu Jan Hoffmann and Yiyang Guo. 2026. Artifact for "Handling Exceptions and Effects with Automatic Resource Analysis". https://doi.org/10.5281/zenodo.18742777 10.5281/zenodo.18742777
10.5281/zenodo.18742777
[27]
Ezgi Çiçek, Deepak Garg, and Umut A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP’15).
[28]
Karl Crary and Stephanie Weirich. 2000. Resource Bound Certification. In 27th ACM Symp. on Principles of Prog. Langs. (POPL’00). 184–198.
[29]
[30]
Ugo Dal Lago and Simone Martini. 2006. An Invariant Cost Model for the Lambda Calculus. In Logical Approaches to Computational Barriers, Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 105–114. isbn:978-3-540-35468-0
[31]
Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL’08).
[35]
[38]
Inc. Facebook. 2024. Infer Website - Cost: Runtime Complexity Analysis. https://fbinfer.com/docs/checker-cost
[39]
[40]
Antonio Flores-Montoya and Reiner Hähnle. 2014. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposiu (APLAS’14).
[41]
Florian Frohn, M. Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl. 2016. Lower Runtime Bounds for Integer Programs. In Automated Reasoning - 8th International Joint Conference (IJCAR’16).
[43]
Bernd Grobauer. 2001. Cost Recurrences for DML Programs. In 6th Int. Conf. on Funct. Prog. (ICFP’01). 253–264.
[44]
[45]
Jessie Grosen, David Kahn, and Jan Hoffmann. 2023. Automatic Amortized Resource Analysis with Regular Recursive Types. In 38th ACM/IEEE Symposium on Logic in Computer Science (LICS’ 23).
[46]
Sumit Gulwani, Sagar Jain, and Eric Koskinen. 2009. Control-Flow Refinement and Progress Invariants for Bound Analysis. In Conf. on Prog. Lang. Design and Impl. (PLDI’09).
[47]
Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th ACM Symp. on Principles of Prog. Langs. (POPL’09).
[48]
Sumit Gulwani and Florian Zuleger. 2010. The Reachability-Bound Problem. In Conf. on Prog. Lang. Design and Impl. (PLDI’10).
[49]
[50]
Robert Harper. 2012. Practical Foundations for Programming Languages. Cambridge University Press. isbn:9781107029576
Showing 50 of 110 references
Metrics
0
Citations
110
References
Details
- Published
- Apr 10, 2026
- Vol/Issue
- 10(OOPSLA1)
- Pages
- 201-230
Authors
Cite This Article
Ethan Chu, Yiyang Guo, Jan Hoffmann (2026). Handling Exceptions and Effects with Automatic Resource Analysis. Proceedings of the ACM on Programming Languages, 10(OOPSLA1), 201-230. https://doi.org/10.1145/3798207
Related
You May Also Like
code2vec: learning distributed representations of code
Uri Alon, Meital Zilberstein · 2019
880 citations
Grounded Copilot: How Programmers Interact with Code-Generating Models
Shraddha Barke, Michael B. James · 2023
275 citations