Skip to main content

Research Repository

See what's under the surface

Professor GRAHAM HUTTON


Liquidate your assets: reasoning about resource usage in liquid Haskell (2019)
Journal Article
Handley, M., Vazou, N., & Hutton, G. (2019). Liquidate your assets: reasoning about resource usage in liquid Haskell. Proceedings of the ACM on Programming Languages, 4, 1-27. https://doi.org/10.1145/3371092

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 pro... Read More about Liquidate your assets: reasoning about resource usage in liquid Haskell.

Call-by-need is clairvoyant call-by-value (2019)
Journal Article
Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages, 3(ICFP), 1-21. https://doi.org/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 about Call-by-need is clairvoyant call-by-value.

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 about AutoBench: comparing the time performance of Haskell programs.

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 about Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl).

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 about Parametric polymorphism and operational improvement.

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 about Compiling a 50-year journey.

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 about Failing faster: overlapping patterns for property-based testing.

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 about Towards a theory of reach.

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 about Cutting out continuations.

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 about Contractive functions on infinite data structures.