Skip to main content

Research Repository

Advanced Search

Outputs (53)

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.

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.

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.

Fold and Unfold for Program Semantics (1998)
Presentation / Conference Contribution
Hutton, G. Fold and Unfold for Program Semantics. Presented at Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming

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 about Fold and Unfold for Program Semantics.