Jeremy Gibbons

Chapter 8 Algebraic Methods for Optimization Problems (2009)

Richard Bird, Jeremy Gibbons, Shin-cheng Mu

Abstract. We argue for the benefits of relations over functions for modelling programs, and even more so for modelling specifications. To support this argument, we present an extended case study for...

ABSTRACT Semantic Frameworks for e-Government (2008)

Charles Crichton, Jim Davies, Jeremy Gibbons, Steve Harris, Aadya Shukla

This paper explains how semantic frameworks can be used to support successful e-Government initiatives by connecting system design to a shared understanding of interactions and processes. It shows...

On Specifying and Visualising Long Running Empirical Studies (2008)

Jeremy Gibbons

In this paper we describe a graphical approach to formally specifying temporally-ordered activity routines designed for calendar scheduling. We introduce a workflow model OWorkflow, for constructing...

Unfolding Abstract Datatypes (2008)

Jeremy Gibbons

Abstract. One of the most fundamental tools in the programmer’s toolbox is the abstract datatype. However, abstract datatypes are not as widely used in functional programming as they might be,...

Under consideration for publication in J. Functional Programming 1 The Essence of the Iterator Pattern (2008)

Jeremy Gibbons

The ITERATOR pattern gives a clean interface for element-by-element access to a collection, independent of the collection’s shape. Imperative iterations using the pattern have two simultaneous...

Generic and Indexed Programming (Project Paper) (2008)

Jeremy Gibbons, Meng Wang

The EPSRC-funded Generic and Indexed Programming project will explore the interaction between datatype-generic programming (DGP) — programs parametrized by the shape of their data — and indexed...

Unifying Theories of Objects (2008)

Michael Anthony Smith, Jeremy Gibbons

Abstract. We present an approach to modelling Abadi–Cardelli-style object calculi as Unifying Theories of Programming (UTP) designs. Here we provide a core object calculus with an operational...

Cross-Trial Query System for Cancer Clinical Trials (2008)

Radu Calinescu, Steve Harris, Jeremy Gibbons, Jim Davies

Abstract Data sharing represents one of the key objectives and major challenges of today’s cancer research. CancerGrid, a consortium of clinicians, cancer researchers, computational biologists and...

Revised Lectures (2008)

J. Van Leeuwen, Jeremy Gibbons, Ralf Hinze, Johan Jeuring (eds

A leitmotif in the evolution of programming paradigms has been the level and extent of parametrisation that is facilitated — the so-called genericity of the paradigm. The sorts of parameters that...

CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES (2008)

Jeremy Gibbons

The public defense will take place on Sept. 3, 2000.

IOS Press Proof Methods for Corecursive Programs (2008)

Jeremy Gibbons

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

Towards Acoli25-44 Semanti4 for Vi25 Programmi2 (2008)

Jeremy Gibbons

Sov ware architects such as Garlan and Katz pro617 the separatio o computationfro coor dination. They encoC)6, the study connector as first-class entities,and super ositiono cotny,)1C o nto co; o; ts...

Under consideration for publication in J. Functional Programming The Essence of the Iterator Pattern (2008)

Jeremy Gibbons

The ITERATOR pattern gives a clean interface for element-by-element access to a collection, independent of the collection’s shape. Imperative iterations using the pattern have two simultaneous...

Report Series (2007)

Jeremy Gibbons, Jeremy Gibbons

An initial-algebra approach to directed acyclic graphs

More on Merging and Selection (2007)

Jeremy Gibbons School, Jeremy Gibbons

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

Dotted and Dashed Lines in METAFONT (2007)

Jeremy Gibbons

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

Program Optimisation, Naturally (2007)

Richard Bird, Jeremy Gibbons, Geraint Jones

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

Chapter 5 Calculating Functional Programs (2007)

Jeremy Gibbons

Abstract. Functional programs are merely equations; they may be manipulated by straightforward equational reasoning. In particular, one can use this style of reasoning to calculate programs, in the...

A monadic interpretation of tactics (2007)

Andrew Martin, Jeremy Gibbons

Abstract. Many proof tools use ‘tactic languages ’ as programs to direct their proofs. We present a simplified idealised tactic language, and describe its denotational semantics. The language has...

b (2007)

Jeremy Gibbons, 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...

Enumerating the Rationals (2007)

Jeremy Gibbons, Richard Bird

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

Patterns in datatype-generic programming (extended abstract) (2007)

Jeremy Gibbons

Generic programming [14, 10] is a matter of making programs more adaptable by making them more

Streaming Algorithms (Extended Abstract) (2007)

Jeremy Gibbons

Unfolds generate data structures, and folds consume them.

The essence of the Iterator pattern (2006)

Jeremy Gibbons

The ITERATOR pattern gives a clean interface for element-by-element access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various...

Design Patterns as Higher-Order Datatype-Generic Programs (2006)

Jeremy Gibbons

Design patterns are reusable abstractions in object-oriented software. However, using current programming languages, these elements can only be expressed extra-linguistically: as prose, pictures, and...

Fission for Program Comprehension (2006)

Jeremy Gibbons Oxford, Jeremy Gibbons

Fusion is a program transformation that combines adjacent computations, flattening structure and improving e#ciency at the cost of clarity. Fission is the same transformation, in reverse: creating...

The essence of the Iterator pattern (2006)

Jeremy Gibbons

The ITERATOR pattern gives a clean interface for element-by-element access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various...

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

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)

Jeremy Gibbons

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)

Jeremy Gibbons, Graham Hutton

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

Metamorphisms: Streaming Representation-Changers (2005)

Jeremy Gibbons

Unfolds generate data structures, and folds consume them. A hylomorphism is a fold after an unfold, generating then consuming a virtual data structure. A metamorphism is the opposite composition, an...

Streaming Representation-Changers (2004)

Jeremy Gibbons

Unfolds generate data structures, and folds consume them.

An unbounded spigot algorithm for the digits of π (2003)

Jeremy Gibbons

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

Arithmetic coding with folds and unfolds (2003)

Richard Bird, Jeremy Gibbons

Arithmetic coding is a method for data compression. Although the idea was

On the supervision and assessment of part-time postgraduate software engineering projects (2003)

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

Patterns in Datatype-Generic Programming (2003)

Jeremy Gibbons

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

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

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

The generic approximation lemma (2001)

Graham Hutton, Jeremy Gibbons

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

Pointwise Relational Programming (2000)

Oege De Moor, Jeremy Gibbons

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

Pointwise Relational Programming (2000)

Oege De Moor, Jeremy Gibbons

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

On the Semantics of Nested Datatypes (2000)

Clare Martin, Jeremy Gibbons

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)

Oege De Moor, Jeremy Gibbons

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

Generic Downwards Accumulations (2000)

Jeremy Gibbons

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

Calculating Functional Programs (2000)

Jeremy Gibbons

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

Abstract (2000)

Graham Hutton, Jeremy Gibbons

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

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

Proof Methods for Structured Corecursive Programs (1999)

Jeremy Gibbons, Graham Hutton

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)

Jeremy Gibbons, Graham Hutton

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)

Oege De Moor, Jeremy Gibbons

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)

Jeremy Gibbons, Graham Hutton

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

Structured programming in Java (1998)

Jeremy Gibbons School, Jeremy Gibbons

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

A Pointless Derivation of Radix Sort (1998)

Jeremy Gibbons

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 Under-Appreciated Unfold (1998)

Jeremy Gibbons, Geraint Jones

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 (1998)

Jeremy Gibbons, Gipsy Lane Headington

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 Under-Appreciated Unfold (1998)

Jeremy Gibbons, Geraint Jones

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

Bridging the algorithm gap: A linear-time functional program for paragraph formatting (1997)

Oege De Moor, Jeremy Gibbons

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 (1997)

Oege De Moor, Jeremy Gibbons

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

Tracing lazy functional languages (1996)

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.

Computing Downwards Accumulations on Trees Quickly (1996)

Jeremy Gibbons

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

Conditionals in Distributive Categories (1996)

Jeremy Gibbons

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

Tracing Lazy Functional Languages (1996)

Jeremy Gibbons And, 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...

The Third Homomorphism Theorem (1995)

Jeremy Gibbons, Jeremy Gibbons

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 (1995)

Jeremy Gibbons, Jeremy Gibbons

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

Deriving Tidy Drawings of Trees (1995)

Jeremy Gibbons

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

Tracing Lazy Functional Languages (1995)

Jeremy Gibbons, Jeremy Gibbons, Keith Wansbrough, 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...

The Third Homomorphism Theorem (1995)

Jeremy Gibbons

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)

Jeremy Gibbons

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

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

How to Derive Tidy Drawings of Trees (1994)

Jeremy Gibbons

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

Formal Methods: Why Should I Care? - The development of the T800 transputer floating-point unit (1993)

Jeremy Gibbons

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

Linear-time breadth-first tree algorithms: An exercise in the arithmetic of folds and zips (1993)

Geraint Jones, Jeremy Gibbons

. This paper is about an application of the mathematics of the zip, reduce (fold) and accumulate (scan) operations on lists. It gives an account of the derivation of a linear-time breadth-first tree...

Linear-time breadth-first tree algorithms An exercise in the arithmetic of folds and zips (1992)

Geraint Jones, Jeremy Gibbons

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