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)
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)
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,...
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)
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...
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)
The public defense will take place on Sept. 3, 2000.
IOS Press Proof Methods for Corecursive Programs (2008)
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)
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...
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...
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)
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)
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)
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...
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)
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)
Generic programming [14, 10] is a matter of making programs more adaptable by making them more
Streaming Algorithms (Extended Abstract) (2007)
Unfolds generate data structures, and folds consume them.
The essence of the Iterator pattern (2006)
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)
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)
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)
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)
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)
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)
Unfolds generate data structures, and folds consume them.
An unbounded spigot algorithm for the digits of π (2003)
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)
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)
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...
On the semantics of nested datatypes (2001)
Clare Martin, Jeremy Gibbons, Ian Bayley
Disciplined, efficient, generalised folds
The generic approximation lemma (2001)
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)
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)
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)
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 specic applications, the calculus can be rather...
Generic Downwards Accumulations (2000)
. 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)
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...
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)
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)
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...
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...
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)
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)
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)
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)
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)
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)
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)
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)
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)
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...
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)
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...
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)
. 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)
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...