My Research

I'm a postdoctoral researcher in the Functional Programming Lab working on the Mind the Gap project funded by the EPSRC. This project aims to develop abstract ways of reasoning about program efficiency that are compatible with the current state-of-the-art techniques used to reason about correctness. Currently most program optimisations are justified using empirical techniques such as benchmarks; this project hopes to put the science of program efficiency on a more rigorous footing.

Ultimately, I would like to generalise ideas from algebraic improvement theories to a categorical (more precisely, 2-categorical or order-enriched-categorical) notion of program improvement, allowing proofs of improvement to be made with the greatest generality. Some of my work on the worker-wrapper transformation uses this idea, and I plan to work further on applying this concept in the future.

I have a particular interest in evaluation strategies. My programming language of choice, Haskell, notably uses a "lazy" evaluation strategy which can make it difficult to reason about operational aspects of programs. It's my hope that by developing theories for reasoning about program efficiency, I can help to diminish this drawback and further encourage the adoption of lazy evaluation strategies. I am also interested in linear and affine lambda calculi for what they can tell us about lazy evaluation strategies.

Papers

Programs for Cheap!
Jennifer Hackett, Graham Hutton
Annual ACM/IEEE Symposium on Logic in Computer Science, 2015
Write down the definition of a recursion operator on a piece of paper. Tell me its type, but be careful not to let me see the operator's definition. I will tell you an optimization theorem that the operator satisfies. As an added bonus, I will also give you a proof of correctness for the optimisation, along with a formal guarantee about its effect on performance. The purpose of this paper is to explain these tricks.

Worker/Wrapper/Makes it/Faster
Jennifer Hackett, Graham Hutton
International Conference on Functional Programming, 2014
Much research in program optimisation has focused on formal approaches to correctness: proving that the meaning of programs is preserved. Paradoxically, there has been little work on formal approaches to efficiency: proving that the performance of optimised programs is actually improved. This paper addresses this problem for a general-purpose optimization technique, the worker/wrapper transformation. In particular, we use improvement theory to establish conditions under which the worker/wrapper transformation is formally guaranteed to improve the time performance of programs. These conditions are a natural refinement of those that guarantee the correctness of the transformation, and the resulting theory is simple to understand and apply.

The Underperforming Unfold: A New Approach to Optimising Recursive Programs
Jennifer Hackett, Graham Hutton, Mauro Jaskelioff
Symposium on Implementation and Application of Functional Languages, 2013
This paper presents a new approach to optimising corecursive programs by factorisation. In particular, we focus on programs written using the corecursion operator unfold. We use and expand upon the proof techniques of guarded coinduction and unfold fusion, capturing a pattern of generalising coinductive hypotheses by means of abstraction and representation functions. The pattern we observe is simple, has not been observed before, and is widely applicable. We develop a general program factorisation theorem from this pattern, demonstrating its utility with a range of practical examples.

Bio

I was born and grew up in Southampton, Hampshire, but fled to Oxford to do my undergraduate degree in Computer Science. I achieved top first for my first three years and a first class degree overall. However, in search of a change of scene I once again fled, this time to Nottingham for a PhD! People have been criticising me for this decision ever since.

Outside of the world of computer science I have been involved in various student activism, including protesting the right-wing group Christian Concern when they came to Oxford for a conference, and being involved in Oxford University's Gender Inclusion Campaign. This has continued in Nottingham, where I held a position on the Student Union's LGBT Network Committee. I also attended NUS LGBT Conference 2013, and was involved in the campaign to create a Trans* Officer and dedicated trans* conference in NUS.

I am into music, with my tastes ranging widely from anarcho-pop band Chumbawamba through 20th century classical composers such as Béla Bartók and avant-rockers Thinking Plague all the way to jazz-musician-cum-rapper Soweto Kinch. I also play guitar and have mysterious and subtle links to a breakdancer named Ereshkigal.

I tweet under the name @lambdagrrl.

Contact

Departmental E-Mail

jph AT cs DOT nott DOT ac DOT uk

My Oxford alumna e-mail (should you wish to flatter/embarrass me)

jennifer DOT hackett AT cs DOT oxon DOT org

My Office

A02, Functional Programming Lab, School of Computer Science, Jubilee Campus, University of Nottingham


School of Computer Science and Information Technology Home Page

The University of Nottingham Home Page