Skip to main content

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

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

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

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

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 (2005)
Conference Proceeding
Hutton, G., & Wright, J. (2005). Calculating an Exceptional Machine

In previous work we showed how to verify a compiler for a small language with exceptions. In this article we show how to calculate, as opposed to verify, an abstract machine for this language. The key step is the use of Reynold's defunctionalizatio... Read More

Accurate Step Counting (2005)
Conference Proceeding
Hope, C., & Hutton, G. (2005). Accurate Step Counting

Starting with an evaluator for a language, an abstract machine for the same language can be mechanically derived using successive program transformations. This has relevance to studying both the space and time properties of programs because these ca... Read More

Compiling Exceptions Correctly (2004)
Conference Proceeding
Hutton, G., & Wright, J. (2004). Compiling Exceptions Correctly

Exceptions are an important feature of modern programming languages, but their compilation has traditionally been viewed as an advanced topic. In this article we show that the basic method of compiling exceptions using stack unwinding can be explain... Read More

When is a function a fold or an unfold? (2001)
Conference Proceeding
Gibbons, J., Hutton, G., & Altenkirch, T. (2001). When is a function a fold or an unfold?

We give a necessary and sufficient condition for when a set-theoretic function can be written using the recursion operator fold, and a dual condition for the recursion operator unfold. The conditions are simple, practically useful, and generic in the... Read More

Proof methods for structured corecursive programs (1999)
Conference Proceeding
Gibbons, J., & Hutton, G. (1999). Proof methods for structured corecursive programs

Corecursive programs produce values of greatest fixpoint types, in contrast to recursive programs, which consume values of least fixpoint types. There are a number of widely used methods for proving properties of corecursive programs, including fixp... Read More

Fold and Unfold for Program Semantics (1998)
Conference Proceeding
Hutton, G. (1998). Fold and Unfold for Program Semantics

In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how th... Read More

Bananas in space: extending fold and unfold to exponential types (1995)
Conference Proceeding
Meijer, E., & Hutton, G. (1995). Bananas in space: extending fold and unfold to exponential types

Fold and unfold are general purpose functionals for process-ing and constructing lists. By using the categorical approach of modelling recursive datatypes as fixed points of functors, these functionals and their algebraic properties were generalised... Read More