All Outputs (52)

The under-performing unfold: a new approach to optimising corecursive programs (2013)
Conference Proceeding

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)
Conference Proceeding

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)
Conference Proceeding

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

Compact fusion (2006)
Conference Proceeding

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

Report on BCTCS 2005 (2005)
Journal Article

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

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.

Accurate Step Counting (2005)
Conference Proceeding

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

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

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

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

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)
Conference Proceeding

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

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)
Conference Proceeding

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

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.

Fold and Unfold for Program Semantics (1998)
Conference Proceeding

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.

Back to Basics: Deriving Representation Changers Functionally (1996)
Journal Article

Many functional programs can be viewed as representation changers, that is, as functions that convert abstract values from one concrete representation to another. Examples of such programs include base-converters, binary adders and multipliers, and... Read More about Back to Basics: Deriving Representation Changers Functionally.

Monadic parser combinators (1996)
Book

In functional programming, a popular approach to building recursive descent parsers is to model parsers as functions, and to define higher-order functions (or combinators) that implement grammar constructions such as sequencing, choice, and repetitio... Read More about Monadic parser combinators.