I'm a second year PhD student within the School of Computer Science.
I'm a member of the Functional Programming Lab research group.
I'm trying to observe the mathematical structure of computation: helping me
are my supervisers Professor Graham Hutton and Professor Thorsten Altenkirch.
Send me an email if you can help too: martin (dot) handley (at) nottingham.ac.uk.
Improving Haskell (pdf)
Martin Handley and Graham Hutton.
Submitted to the European Symposium on Programming, 2017.
Lazy evaluation is a key feature of Haskell, but can make it difficult to reason about the operational efficiency of programs. Improvement theory addresses this problem by providing a foundation for proofs of program improvement in a call-by-need setting, and has recently been the subject of renewed interest. However, proofs of improvement are intricate and require an inequational style of reasoning that is unfamiliarto most Haskell programmers. In this article, we present the design and implementation of an inequational reasoning assistant that provides mechanical support for improvement proofs, and demonstrate its utility by verifying a range of improvement results from the literature.