Here’s an interesting short paper by Wadler: Lazy vs. strict. Philip Wadler. ACM Computing Surveys, June 1996. To paraphrase, the simplest model of lazy evaluation is given by Church’s original $\lambda$ calculus, and the simplest model of strict evaluation is given by Plotkin’s $\lambda_v$ calculus. $\lambda$ is problematic because it gives a poor notion of the cost of programs, and $\lambda_v$ is problematic because it is not complete. These flaws can be removed at the cost of slightly more complicated models, and the resulting models turn out to be extremely similar.