One of the key benefits of functional programming languages is the ability to reason about programs in a formal manner. However, while the high-level nature of the functional paradigm simplifies reasoning about program correctness, it also makes it more difficult to reason about program efficiency. This reasoning gap is particularly pronounced in lazy languages such as Haskell, where the on-demand nature of evaluation makes reasoning about efficiency even more challenging. We have recently shown how a theory of program improvement can be used to address this problem, demonstrating the feasibility of a unified approach to reasoning that allows both correctness and efficiency to be considered in the same general framework. The aim of this project is to build on the success of this work and develop new high-level techniques for reasoning about functional programs that bridge the correctness/efficiency gap. The project will fund a named researcher for four years, is supported by a fully-funded PhD studentship from the host institution, and is enhanced by a team of leading international collaborators.