All Outputs (55)

Programs for cheap! (2015)
Presentation / Conference Contribution
Hackett, J., & Hutton, G. (2015, July). Programs for cheap!. Presented at Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science, Kyoto, Japan

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!.

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), https://doi.org/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 about Work it, wrap it, fix it, fold it.

Worker/wrapper/makes it/faster (2014)
Presentation / Conference Contribution
Hackett, J., & Hutton, G. Worker/wrapper/makes it/faster. Presented at ACM SIGPLAN International Conference on Functional Programming (19th)

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)
Presentation / Conference Contribution
Hackett, J., Hutton, G., & Jaskelioff, M. The under-performing unfold: a new approach to optimising corecursive programs. Presented at International Symposium on Implementation and Application of Functional Languages (25th)

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.

Towards modular compilers for effects (2012)
Presentation / Conference Contribution
Day, L., & Hutton, G. Towards modular compilers for effects. Presented at International Symposium on Trends in Functional Programming (12th)

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 about Towards modular compilers for effects.

Compiling concurrency correctly: cutting out the middle man (2010)
Presentation / Conference Contribution
Hu, L., & Hutton, G. Compiling concurrency correctly: cutting out the middle man. Presented at Symposium on Trends in Functional Programming (10th)

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.

Programming in Haskell (2007)
Book
Hutton, G. (2007). Programming in Haskell. Cambridge University Press

Compact fusion (2006)
Presentation / Conference Contribution
Hope, C., & Hutton, G. Compact fusion. Presented at Workshop on Mathematically Structured Functional Programming

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.

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

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.

Proof Methods for Corecursive Programs (2005)
Journal Article
Hutton, G., & Gibbons, J. (2005). Proof Methods for Corecursive Programs

Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main m... Read More about Proof Methods for Corecursive Programs.

Calculating an Exceptional Machine (2005)
Presentation / Conference Contribution
Hutton, G., & Wright, J. Calculating an Exceptional Machine. Presented at Proceedings of the Fifth Symposium on Trends in Functional Programming

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.

Accurate Step Counting (2005)
Presentation / Conference Contribution
Hope, C., & Hutton, G. Accurate Step Counting. Presented at 17th International Workshop on Implementation and Application of Functional Languages

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.

Compiling Exceptions Correctly (2004)
Presentation / Conference Contribution
Hutton, G., & Wright, J. Compiling Exceptions Correctly. Presented at Proceedings of the 7th International Conference on Mathematics of Program Construction

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.

The Countdown Problem (2002)
Journal Article
Hutton, G. (2002). The Countdown Problem. Journal of Functional Programming, 12(6),

We systematically develop a functional program that solves the countdown problem, a numbers game in which the aim is to construct arithmetic expressions satisfying certain constraints. Starting from a formal specification of the problem, we present... Read More about The Countdown Problem.

The Generic Approximation Lemma (2001)
Journal Article
Hutton, G., & Gibbons, J. (2001). The Generic Approximation Lemma. Information Processing Letters, 79(4), https://doi.org/10.1016/S0020-0190%2800%2900220-9

The approximation lemma is a simplification of the well-known take lemma, and is used to prove properties of programs that produce lists of values. We show how the approximation lemma, unlike the take lemma, can naturally be generalised from lists t... Read More about The Generic Approximation Lemma.

When is a function a fold or an unfold? (2001)
Presentation / Conference Contribution
Gibbons, J., Hutton, G., & Altenkirch, T. When is a function a fold or an unfold?. Presented at Workshop on Coalgebraic Methods in Computer Science (4th)

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 about When is a function a fold or an unfold?.

A Tutorial on the Universality and Expressiveness of Fold (1999)
Journal Article
Hutton, G. (1999). A Tutorial on the Universality and Expressiveness of Fold. Journal of Functional Programming, 9(4), https://doi.org/10.1017/s0956796899003500

In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the uni... Read More about A Tutorial on the Universality and Expressiveness of Fold.

Proof methods for structured corecursive programs (1999)
Presentation / Conference Contribution
Gibbons, J., & Hutton, G. Proof methods for structured corecursive programs. Presented at 1st Scottish Functional Programming Workshop

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 about Proof methods for structured corecursive programs.

Monadic parsing in Haskell (1998)
Journal Article
Hutton, G., & Meijer, E. (1998). Monadic parsing in Haskell. Journal of Functional Programming, 8(4), https://doi.org/10.1017/s0956796898003050

This paper is a tutorial on defining recursive descent parsers in Haskell. In the spirit of one-stop shopping, the paper combines material from three areas into a single source. The three areas are functional parsers, the use of monads to structure... Read More about Monadic parsing in Haskell.