Research Repository

See what's under the surface


Call-by-need is clairvoyant call-by-value (2019)
Conference Proceeding
Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. doi:10.1145/3341718

Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics, which uses a heap to memoise the results of delayed... Read More

AutoBench: comparing the time performance of Haskell programs (2018)
Conference Proceeding
HANDLEY, M., & HUTTON, G. (2018). AutoBench: comparing the time performance of Haskell programs. In Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18), 26-37. doi:10.1145/3242744.3242749

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 pr... Read More

Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl) (2018)
Conference Proceeding
VAZOU, N., BREITNER, J., KUNKEL, R., VAN HORN, D., & HUTTON, G. (2018). Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl). In Proceedings of the 11th ACM SIGPLAN Haskell Symposium (Haskell '18), 132-144. doi:10.1145/3242744.3242756

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows ho... Read More

Parametric polymorphism and operational improvement (2018)
Conference Proceeding
Hackett, J., & Hutton, G. (2018). Parametric polymorphism and operational improvement. doi:10.1145/3236763

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 f... Read More

Compiling a 50-year journey (2017)
Journal Article
Hutton, G., & Bahr, P. (2017). Compiling a 50-year journey. Journal of Functional Programming, 27,

Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based... Read More

Failing faster: overlapping patterns for property-based testing (2017)
Conference Proceeding
Fowler, J., & Hutton, G. (2017). Failing faster: overlapping patterns for property-based testing. In Practical Aspects of Declarative Languages: 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017: Proceedings, 103-119. doi:10.1007/978-3-319-51676-9-7

In property-based testing, a key problem is generating input data that satisfies the precondition of a property. One approach is to attempt to do so automatically, from the definition of the precondition itself. This idea has been realised using the... Read More

Towards a theory of reach (2016)
Journal Article
Fowler, J., & Hutton, G. (2016). Towards a theory of reach. Lecture Notes in Artificial Intelligence, 9547, doi:10.1007/978-3-319-39110-6

When testing a program, there are usually some parts that are rarely executed and hence more difficult to test. Finding inputs that guarantee that such parts are executed is an example of a reach problem, which in general seeks to ensure that targete... Read More

Cutting out continuations (2016)
Conference Proceeding
Hutton, G., & Bahr, P. (2016). Cutting out continuations

In the field of program transformation, one often transforms programs into continuation-passing style to make their flow of control explicit, and then immediately removes the resulting continuations using defunctionalisation to make the programs firs... Read More

Contractive functions on infinite data structures (2016)
Conference Proceeding
Capretta, V., Hutton, G., & Jaskelioff, M. (in press). Contractive functions on infinite data structures. doi:10.1145/3064899.3064900

Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they... Read More

Calculating correct compilers (2015)
Journal Article
Bahr, P., & Hutton, G. (2015). Calculating correct compilers. Journal of Functional Programming, 25(e14), doi:10.1017/S0956796815000180

In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all deta... Read More

Programs for cheap! (2015)
Conference Proceeding
Hackett, J., & Hutton, G. (2015). Programs for cheap!

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 g... Read More

Work it, wrap it, fix it, fold it (2014)
Journal Article
Sculthorpe, N., & Hutton, G. (2014). Work it, wrap it, fix it, fold it. Journal of Functional Programming, 24(1), doi:10.1017/S0956796814000045

The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different cor... Read More

Worker/wrapper/makes it/faster (2014)
Conference Proceeding
Hackett, J., & Hutton, G. (2014). Worker/wrapper/makes it/faster

Much research in program optimization has focused on formal approaches to correctness: proving that the meaning of programs is preserved by the optimisation. Paradoxically, there has been comparatively little work on formal approaches to efficiency:... Read More

The under-performing unfold: a new approach to optimising corecursive programs (2013)
Conference Proceeding
Hackett, J., Hutton, G., & Jaskelioff, M. (2013). The under-performing unfold: a new approach to optimising corecursive programs

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 f... Read More

Towards modular compilers for effects (2012)
Conference Proceeding
Day, L., & Hutton, G. (2012). Towards modular compilers for effects

Compilers are traditionally factorised into a number of separate phases, such as parsing, type checking, code generation, etc. However, there is another potential factorisation that has received comparatively little attention: the treatment of separa... Read More

Compiling concurrency correctly: cutting out the middle man (2010)
Conference Proceeding
Hu, L., & Hutton, G. (2010). Compiling concurrency correctly: cutting out the middle man

The standard approach to proving compiler correctness for concurrent languages requires the use of multiple translations into an intermediate process calculus. We present a simpler approach that avoids the need for such an intermediate language, usin... Read More

Compact fusion (2006)
Conference Proceeding
Hope, C., & Hutton, G. (2006). Compact fusion

There are many advantages to writing functional programs in a compositional style, such as clarity and modularity. However, the intermediate data structures produced may mean that the resulting program is inefficient in terms of space. These may be r... Read More

Calculating an exceptional machine (2006)
Book Chapter
Hutton, G., & Wright, J. (2006). Calculating an exceptional machine. In H. Loidl (Ed.), Trends in functional programming. Volume 5Intellect

Report on BCTCS 2005 (2005)
Journal Article
Hutton, G. (2005). Report on BCTCS 2005

This report contains edited abstracts from BCTCS 2005, which was held on 22nd to 24th March 2005 in Nottingham, England.