Skip to main content

Research Repository

Advanced Search

All Outputs (23)

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). https://doi.org/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). https://doi.org/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).

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). https://doi.org/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.

Contractive Functions on Infinite Data Structures (2016)
Conference Proceeding
Capretta, V., Hutton, G., & Jaskelioff, M. (2016). Contractive Functions on Infinite Data Structures. In IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages (1-13). https://doi.org/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.

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.

Programs for cheap! (2015)
Conference Proceeding
Hackett, J., & Hutton, G. (2015). Programs for cheap!. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (115-126). https://doi.org/10.1109/LICS.2015.21

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 about Programs for cheap!.

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 about Worker/wrapper/makes it/faster.

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 about The under-performing unfold: a new approach to optimising corecursive programs.

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 about Compiling concurrency correctly: cutting out the middle man.

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 about Compact fusion.

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 about Accurate Step Counting.

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 about Calculating an Exceptional Machine.

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 about Compiling Exceptions Correctly.

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 about Bananas in space: extending fold and unfold to exponential types.