Mind the Gap: Unified Reasoning About Program Correctness and Efficiency

Lead Research Organisation: University of Nottingham
Department Name: School of Computer Science


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.

Planned Impact

We expect impact in the following areas:

1. EPSRC has a goal of growing its research in 'Verification and Correctness' and 'Programming Languages and Compilers', and this project contributes directly, and immediately, to this goal. The project also contributes immediately to UKCRC grand challenge GC6, which seeks basic scientific principles for verifying the behaviour of software systems.

2. Researchers working in the area of functional programming languages will be the next most immediate beneficiaries of our work, as described in 'academic beneficiaries' above. By focusing on a key understudied problem in the field, the project will open up new avenues of research for the academic community.

3. Functional programmers interested in understanding and improving the performance of their programs will be able to take direct advantage of our results through the new techniques and tools that we develop, which will give new ways to formally reason about efficiency that complement existing techniques for correctness.

4. Finally, the impact of our work will be significantly enhanced through our programme of education actvities, which includes an improvement handbook, video lectures, and organisation of an international Summer school.


10 25 50
publication icon
Handley M (2018) AutoBench: comparing the time performance of Haskell programs in ACM SIGPLAN Notices

publication icon
BAHR P (2020) Calculating correct compilers II: Return of the register machines in Journal of Functional Programming

publication icon
Pickard M (2021) Calculating dependently-typed compilers (functional pearl) in Proceedings of the ACM on Programming Languages

publication icon
Hackett J (2019) Call-by-need is clairvoyant call-by-value in Proceedings of the ACM on Programming Languages

publication icon
Hutton G (2017) Compiling a 50-year journey in Journal of Functional Programming

publication icon
Handley M (2018) Improving Haskell