Proof Methods for Corecursive Programs (2005)
Hutton, Graham, Gibbons, Jeremy
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...
Proof Methods for Corecursive Programs (2005)
Hutton, Graham, Gibbons, Jeremy
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...
Enumerating the Rationals (2004)
We present a series of lazy functional programs for enumerating the rational numbers without duplication, drawing on some elegant results of Neil Calkin, Herbert Wilf and Moshe Newman.
The Fun of Programming Oege de Moor, (2004)
Contents Fun with phantom types 5 Fun with phantom types Haskell is renowned for its many extensions to the Hindley-Milner type system (type classes, polymorphic recursion, rank-n types, existential...
Unbounded Spigot Algorithms for the Digits of π (2004)
Rabinowitz and Wagon (in American Mathematical Monthly 102(3):195--203, 1995) present a spigot algorithm for computing the digits of #. A spigot algorithm yields its outputs incrementally, and does...
Streaming Representation-Changers (2004)
Unfolds generate data structures, and folds consume them.
Patterns in Datatype-Generic Programming (extended abstract) (2004)
This paper describes the work to be undertaken in the UK EPSRC-funded project Datatype Generic Programming, starting October 2003. The work described in this paper will constitute about a third of...
Streaming Algorithms (Extended Abstract) (2004)
Unfolds generate data structures, and folds consume them.
Patterns in Datatype-Generic Programming (2003)
Generic programming consists of increasing the expressiveness of programs by allowing a wider variety of kinds of parameter than is usual. The most popular instance of this scheme is the C++ Standard...
Arithmetic Coding With Folds and Unfolds (2003)
Introduction Arithmetic coding is a method for data compression. Although the idea was developed in the 1970's, it wasn't until the publication of an "accessible implementation " [14] that it...
On The Supervision and Assessment Of Part-Time Postgraduate Software Engineering Projects (2002)
Andrew Simpson, Andrew Martin, Jeremy Gibbons, Jim Davies, Steve Mckeever
This paper describes existing practices in the supervision and assessment of projects undertaken by part-time, postgraduate students in Software Engineering. It considers this aspect of the learning...
Disciplined, Efficient, Generalised Folds for Nested Datatypes (2002)
Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson...
The Generic Approximation Lemma (2001)
Hutton, Graham, Gibbons, Jeremy
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...
The Generic Approximation Lemma (2001)
Hutton, Graham, Gibbons, Jeremy
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...
When is a Function a Fold Or an Unfold? (2001)
Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch
We give a necessary and su#cient 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...
When is a Function a Fold Or an Unfold? (2001)
Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch
We give a necessary and su#cient 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...
When is a function a fold or an unfold? (DRAFT of January 3, 2001) (2001)
Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch
We give a necessary and su#cient 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...
Proof Methods for Corecursive Programs (2000)
This article is a tutorial on four methods for proving properties of corecursive programs: fixpoint induction, the approximation lemma, coinduction, and fusion.
Pointwise Relational Programming (2000)
. The point-free relational calculus has been very successful as a language for discussing general programming principles. However, when it comes to specic applications, the calculus can be rather...
On the Semantics of Nested Datatypes (2000)
Introduction Nested datatypes were introduced in [1] as recursively dened parameterised datatypes in which the parameter of the datatype changes in the recursive call. For example, the Nest datatype,...
Pointwise Relational Programming (2000)
The point-free relational calculus has been very successful as a language for discussing general programming principles. However, when it comes to specific applications, the calculus can be rather...
Program Optimisation, Naturally (2000)
this paper we derive another, quite di#erent, linear-time algorithm for reversing a list. The derivation relies on a higherorder naturality [5] property of the function unzip, the function that turns...
Pointwise Relational Programming (2000)
The point-free relational calculus has been very successful as a language for discussing general programming principles. However, when it comes to specific applications, the calculus can be rather...
The Generic Approximation Lemma (2000)
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...
The Generic Approximation Lemma (2000)
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...
Computing Downwards Accumulations on Trees Quickly (1999)
. Downwards accumulations on binary trees are essentially functions which pass information down a tree, from the root towards the leaves. Under certain conditions, a downwards accumulation is both...
Generic Downwards Accumulations (1999)
. A downwards accumulation is a higher-order operation that distributes information downwards through a data structure, from the root towards the leaves. The concept was originally introduced in an...
The Under-Appreciated Unfold (1999)
Folds are appreciated by functional programmers. Their dual, unfolds, are not new, but they are not nearly as well appreciated. We believe they deserve better. To illustrate, we present (indeed, we...
Polytypic Downwards Accumulations (1999)
A downwards accumulation is a higher-order operation that distributes information downwards through a data structure, from the root towards the leaves. The concept was originally introduced in an ad...
The term `formal methods' is a general term for precise mathematically-based techniques used in the development of computer systems, both hardware and software. This paper discusses formal methods in...
Calculating Functional Programs (1999)
A good way of developing a correct program is to calculate it from its specification. Functional programming languages are especially suitable for this, because their referential transparency greatly...
Tracing Lazy Functional Languages (1999)
Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the callby -need lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional...
More on Merging and Selection (1999)
In his paper On Merging and Selection (Journal of Functional Programming 7(3), 1997), Bird considers the problem of computing the nth element of the list resulting from merging the two sorted lists x...
Proof Methods for Structured Corecursive Programs (1999)
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...
Program Optimisation, Naturally (1999)
Richard Bird, Jeremy Gibbons, Geraint Jones
It is well-known that each polymorphic function satises a certain equational law, called a naturality condition. Such laws are part and parcel of the basic toolkit for improving the eÆciency of...
Bridging the Algorithm Gap: A Linear-time Functional Program for Paragraph Formatting (1999)
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the...
Bridging the Algorithm Gap: A Linear-time Functional Program for Paragraph Formatting (1999)
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the...
Proof Methods for Structured Corecursive Programs (1999)
Gibbons, Jeremy, Hutton, Graham
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...
Proof Methods for Structured Corecursive Programs (1999)
Gibbons, Jeremy, Hutton, Graham
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...
Tracing Lazy Functional Languages (1998)
Jeremy Gibbons And, Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the call-by-need lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional...
The Third Homomorphism Theorem (1998)
The Third Homomorphism Theorem is a folk theorem of the constructive algorithmics community. It states that a function on lists that can be computed both from left to right and from right to left is...
Deriving Tidy Drawings of Trees (1998)
The tree-drawing problem is to produce a `tidy' mapping of elements of a tree to points in the plane. In this paper, we derive an efficient algorithm for producing tidy drawings of trees. The...
An Initial-Algebra Approach to Directed Acyclic Graphs (1998)
. The initial-algebra approach to modelling datatypes consists of giving constructors for building larger objects of that type from smaller ones, and laws identifying di#erentways of constructing the...
Computing Downwards Accumulations on Trees Quickly (1998)
Downwards passes on binary trees are essentially functions which pass information down a tree, from the root towards the leaves. Under certain conditions, a downwards pass is both `efficient'...
The Under-Appreciated Unfold (1998)
Folds are appreciated by functional programmers; the benefits of encapsulating common patterns of computation as higher-order operators are well-known and well understood. Their dual, unfolds, are...
The Under-Appreciated Unfold (1998)
Folds are appreciated by functional programmers; the benefits of encapsulating common patterns of computation as higher-order operators are well-known and well understood. Their dual, unfolds, are...
Tracing Lazy Functional Languages (1997)
Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's call-byneed lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional languages. Keywords...
Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's call-byneed lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional languages. Keywords...
Bridging the Algorithm Gap: A Linear-time Functional Program for Paragraph Formatting (1997)
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the...
An Initial-Algebra Approach to (1996)
The initial-algebra approach to modelling datatypes consists of giving constructors for building larger objects of that type from smaller ones, and laws identifying different ways of constructing the...
The Third Homomorphism Theorem (1995)
The Third Homomorphism Theorem is a folk theorem of the constructive algorithmics community. It states that a function on lists that can be computed both from left to right and from right to left is...
An Initial-Algebra Approach to Directed Acyclic Graphs (1995)
. The initial-algebra approach to modelling datatypes consists of giving constructors for building larger objects of that type from smaller ones, and laws identifying different ways of constructing...
Computing Downwards Accumulations on Trees Quickly (1995)
Downwards accumulations on binary trees are essentially functions which pass information down a tree, from the root towards the leaves. Under certain conditions, a downwards accumulation is both...
How to Derive Tidy Drawings of Trees (1994)
The tree-drawing problem is to produce a `tidy' mapping of elements of a tree to points in the plane. In this paper, we derive an efficient algorithm for producing tidy drawings of trees. The...
Efficient Parallel Algorithms for Tree Accumulations (1994)
Jeremy Gibbons, Wentong Cai, David B. Skillicorn
Accumulations are higher-order operations on structured objects; they leave the shape of an object unchanged, but replace elements of that object with accumulated information about other elements....
Linear-time breadth-first tree algorithms An exercise in the arithmetic of folds and zips (1994)
This is a paper about an application of the mathematics of zip, fold (reduce) and accumulate (scan) operations on lists. It gives an account of the derivation of a linear-time breadth-first...
This is a paper about an application of the mathematics of zip, fold (reduce) and accumulate (scan) operations on lists. It gives an account of the derivation of a linear-time breadth-first...
Linear-time breadth-first tree algorithms An exercise in the arithmetic of folds and zips (1994)
This is a paper about an application of the mathematics of zip, fold (reduce) and accumulate (scan) operations on lists. It gives an account of the derivation of a linear-time breadth-first...
Bridging the Algorithm Gap: A Linear-time Functional Program for Paragraph Formatting (1970)
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the...
Dotted and Dashed Lines in METAFONT (1970)
We show how to draw evenly dotted and dashed curved lines in METAFONT, using recursive refinement of paths. METAPOST provides extra primitives that can be used for this task, but the method presented...
Conditionals in Distributive Categories (1970)
In a distributive category (a category in which the product distributes over the coproduct), coproducts can be used to model conditional expressions. We develop such a theory of conditionals. 1...
Structured programming in Java (1970)
We argue that for computing majors, it is better to use a `why' approach to teaching programming than a `how' approach; this involves (among other things) teaching structured programming before...
A Pointless Derivation of Radix Sort (1970)
This paper is about point-free (or `pointless') calculations --- calculations performed at the level of function composition instead of that of function application. We address this topic with the...
Proof Methods for Structured Corecursive Programs (1970)
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...
Efficient Parallel Algorithms for Tree Accumulations (1970)
Jeremy Gibbons, Wentong Cai, David B. Skillicorn
. Accumulations are higher-order operations on structured objects; they leave the shape of an object unchanged, but replace elements of that object with accumulated information about other elements....