We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. as steps
Frédéric Kaplan, Isabella Di Lenardo, Raphaël Barman, Federica Pardini