Mind the Gap: Unified Reasoning About Program Correctness and Efficiency
Lead Research Organisation:
University of Nottingham
Department Name: School of Computer Science
Abstract
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.
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.
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.
Publications
Bahr P
(2022)
Monadic compiler calculation (functional pearl)
in Proceedings of the ACM on Programming Languages
BAHR P
(2020)
Calculating correct compilers II: Return of the register machines
in Journal of Functional Programming
Capretta V
(2016)
Contractive Functions on Infinite Data Structures
Fowler J
(2016)
Failing Faster: Overlapping Patterns for Property-Based Testing
Hackett J
(2018)
Parametric polymorphism and operational improvement
in Proceedings of the ACM on Programming Languages
Hackett J
(2019)
Call-by-need is clairvoyant call-by-value
in Proceedings of the ACM on Programming Languages
Handley M
(2018)
AutoBench: comparing the time performance of Haskell programs
in ACM SIGPLAN Notices
Handley M
(2018)
AutoBench: comparing the time performance of Haskell programs
Handley M
(2019)
Liquidate your assets: reasoning about resource usage in liquid Haskell
in Proceedings of the ACM on Programming Languages
Handley M
(2018)
Improving Haskell
Hutton
(2016)
Programming in Haskell
Hutton G
(2017)
Compiling a 50-year journey
in Journal of Functional Programming
Pickard M
(2021)
Calculating dependently-typed compilers (functional pearl)
in Proceedings of the ACM on Programming Languages