The $\lambda$-calculus is a fundamental model of
computation. It provides a foundation for functional programming.
Therefore, developing an effective cost model for the $\lambda$-calculus is essential
for analysing the complexity of functional code.
The call-by-push-value $\lambda$-calculus allows specifying various evaluation strategies within the
same calculus. This enables programmers to specify how they want their program to evaluate within the calculus.
There has been ongoing research in developing cost models for the $\lambda$-calculus with various evaluation strategies.
Our project aims to extend this line of work by providing an effective
verified cost model for the call-by-push-value $\lambda$-calculus in the HOL4 theorem prover.
As a result, it will allow formal verification of the complexity of functional programs.