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 formal footing.

Recently, I have been looking into metric spaces as models for programming languages, and how this can be used to reason about efficiency.

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

A Generic Foundation for Program Improvement
Jennifer Hackett, Graham Hutton
In preparation, 2018
Improvement theory is an approach to reasoning about program efficiency that allows inequational proofs of improvement to be conducted in a similar manner to equational proofs of correctness. However, there is currently no unified framework for reasoning about efficiency using this approach, with each choice of language, semantics and cost model requiring its own custom theory. This article develops an approach based on metric spaces that is generic in all three of these aspects, allowing us to reason not only about time and space, but any notion of resource. This theory also indicates why space efficiency has been problematic in the past, and shows us how to avoid these problems. We develop our theory and prove a range of generic improvement results, establishing metric spaces as the "essence" of improvement theory.

Parametric Polymorphism and Operational Improvement
Jennifer Hackett, Graham Hutton
In preparation, 2018
Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement, that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to prove time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion.

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 went 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, a fact of which I am eternally embarrassed. After completing my undergraduate degree, I went to the University of Nottingham to do a PhD under the supervision of Graham Hutton, and am now a postdoctoral researcher in the same group.

Outside of the world of computer science I have been involved in various forms of activism. I am involved in the charity organisation Action for Trans Health as well as other forms of LGBTQ+ campaigning. In particular, I was involved in a blockade of the Greater Manchester Police delegation to Manchester Pride 2016. I am also an active member of the Industrial Workers of the World.

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 can be found on the distributed social network Mastodon as @lambdagrrl@scholar.social.

Contact

Departmental E-Mail

jennifer DOT hackett AT nottingham 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