Martin A.T. Handley

I'm a final year PhD student in the Functional Programming Lab at the University of Nottingham. I'm currently researching about new theories for reasoning about program efficiency in a lazy setting, and also developing tools to aid this process. Helping me are my supervisers Professor Graham Hutton and Professor Thorsten Altenkirch.

Please email me if you can help too!


Publications

Liquidate your assets


Reasoning about resource usage in Liquid Haskell

(pdf)
Martin A.T. Handley, Niki Vazou, and Graham Hutton
Submitted to the International Conference on Functional Programming, February 2019.

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program efficiency in the same setting, with the system’s existing verification machinery being used to ensure that the results are both meaningful and precise. To illustrate our approach, we analyse the efficiency of a range of popular data structures and algorithms, and in doing so, explore various notions of resource usage. Our experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and that the two can naturally be combined.

AutoBench


Comparing the time performance of Haskell programs

(pdf)
Martin A.T. Handley and Graham Hutton
Proceedings of the Haskell Symposium, St. Louis, Missouri, USA, June 2018.

Two fundamental goals in programming are correctness (producing the right results) and efficiency (using as few resources as possible). Property-based testing tools such as QuickCheck provide a lightweight means to check the correctness of Haskell programs, but what about their efficiency? In this article, we show how QuickCheck can be combined with the Criterion benchmarking library to give a lightweight means to compare the time performance of Haskell programs. We present the design and implementation of the AutoBench system, demonstrate its utility with a number of case studies, and find that many QuickCheck correctness properties are also efficiency improvements.

Improving Haskell

(pdf)
Martin A.T. Handley and Graham Hutton
Proceedings of the Symposium on Trends in Functional Programming, Gothenburg, Sweden, March 2018.

Lazy evaluation is a key feature of Haskell, but can make it difficult to reason about the 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 unfamiliar to 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.

Software

AutoBench

(github)
Martin A.T. Handley

A lightweight, automated tool for comparing the time performance of Haskell programs. Below is an example use case where we compare the well-known slow and fast reverse functions.

User input:

slowRev_vs._fastRev

System output (to file):

slowRev_vs._fastRev

System output (to console):

slowRev_vs._fastRev

University of Nottingham Improvement Engine (Unie)

(github)
Martin A.T. Handley

A Haskell implemented inequational reasoning assistant that provides mechanical support for proofs of time improvement in a lazy setting. Below is a short video of the system in action.

Teaching

FPL Representative in the PGR-LCF (2017-19)


The LCF aims to ensure that the views of the postgraduate research students are given proper weight and that concerns they may have about supervision, progress, specific training, development opportunities, career, etc. are being addressed.

Teaching Assistant

  • Lab Assistant, Compilers (2017-18)
  • Lab Assistant, Programming in Python (2017-19)
  • Lab Assistant, Systems and Architecture (2016-18)
  • Lab Assistant, Advanced Functional Programming (2016-19)
  • Lab Assistant, Computer Fundamentals (2016-18)
  • Lab Assistant, Computer Security (2016-18)
  • Lab Assistant, Programming Paradigms (2016-19)

Misc.

Impact Magazine Article


Our Mind the Gap project was recently featured in Impact Magazine.

Last updated on 26 April 2019