[1]  R. Calinescu, S. Harris, J. Gibbons, J. Davies, I. Toujilov, and S. Nagl. Modeldriven architecture for cancer research. In 5th IEEE International Conference on Software Engineering and Formal Methods, London, UK, September 1014 2007. 
[2] 
Peter Y. H. Wong and Jeremy Gibbons.
Verifying business process compatibility.
In 3rd International Workshop on Methods and Tools for
Coordinating Concurrent, Distributed and Mobile Systems (MTCoord'07),
Paphos, Cyprus, June 2007.
A shorter version of this paper was presented at the 2nd European
Young Researchers Workshop on Service Oriented Computing, Leicester, United
Kingdom, June 1997.
Business Process Modelling Notation (BPMN), developed by the Business Process Management Initiative (BPMI), intends to bridge the gap between business process design and implementation. In this paper we describe a processalgebraic approach to verifying process interactions for business collaboration described in BPMN. We first describe briefly a process semantics for BPMN in Communicating Sequential Processes; we then use a simple example of business collaboration to demonstrate how our semantic model may be used to verify compatibility between business participants in a collaboration.

[3] 
Jeremy Gibbons.
Datatypegeneric programming.
In Backhouse et al. [4].
[ .pdf ]
Generic programming aims to increase the flexibility of programming languages, by expanding the possibilities for parametrization  ideally, without also expanding the possibilities for uncaught errors. The term means different things to different people: parametric polymorphism, data abstraction, metaprogramming, and so on. We use it to mean polytypism, that is, parametrization by the shape of data structures rather than their contents. To avoid confusion with other uses, we have coined the qualified term datatypegeneric programming for this purpose. In these lecture notes, we expand on the definition of datatypegeneric programming, and present some examples of datatypegeneric programs. We also explore the connection with design patterns in objectoriented programming; in particular, we argue that certain design patterns are just higherorder datatypegeneric programs.

[4]  Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors. Spring School on DatatypeGeneric Programming, volume 4719. SpringerVerlag, 2007. 
[5] 
Michael Anthony Smith and Jeremy Gibbons.
Unifying theories of objects.
In Davies and Gibbons [8], pages
599618.
[ .pdf ]
We present an approach to modelling AbadiCardellistyle object calculi as UTP designs. Here we provide a core object calculus with an operational smallstep evaluation rule semantics, and a corresponding UTP model with a denotational relational predicate semantics. For clarity, the UTP model is defined in terms of an operand stack, which is used to store the results of subprograms. Models of a less operational nature are briefly discussed. The consistency of the UTP model is demonstrated by a structural induction proof over the operations of the core object calculus. Overall, our UTP model is intended to provide facilities for encoding both objectbased and classbased languages.

[6]  Jeremy Gibbons, Meng Wang, and Bruno C. d. S. Oliveira. Generic and indexed programming. In Marco Morazan, editor, Trends in Functional Programming, 2007. [ .pdf ] 
[7] 
Peter Y. H. Wong and Jeremy Gibbons.
A processalgebraic approach to workflow specification and
refinement.
In Software Composition, 2007.
[ .pdf ]
This paper describes a process algebraic approach to specification and refinement of workflow processes. In particular, we model both specification and implementation of workflows as CSP processes. CSP's behavioural models and their respective refinement relations not only enable us to prove correctness properties of an individual workflow process against its behavioural specification, but also allows us to design and develop workflow processes compositionally. Moreover, coupled with CSP is an industrial strength automated model checker FDR, which allows behavioural properties of workflow models to be proved automatically. This paper details some CSP models of van der Aalst et al.'s control flow workflow patterns, and illustrates behavioural specification and refinement of workflow systems with a business process scenario.

[8]  Jim Davies and Jeremy Gibbons, editors. Integrated Formal Methods, volume 4591. SpringerVerlag, 2007. 
[9]  Radu Calinescu, Steve Harris, Jeremy Gibbons, and Jim Davies. Crosstrial query system for cancer clinical trials. In IEEE International Conference on Systems, Computing Sciences and Software Engineering, December 2006. [ http ] 
[10] 
Jeremy Gibbons.
Design patterns as higherorder datatypegeneric programs.
In Ralf Hinze, editor, Workshop on Generic Programming,
September 2006.
[ .pdf ]
Design patterns are reusable abstractions in objectoriented software. However, using current programming languages, these elements can only be expressed extralinguistically: as prose, pictures, and prototypes. We believe that this is not inherent in the patterns themselves, but evidence of a lack of expressivity in the languages of today. We expect that, in the languages of the future, the code part of design patterns will be expressible as reusable library components. Indeed, we claim that the languages of tomorrow will suffice; the future is not far away. The necessary features are higherorder and datatypegeneric constructs; these features are already or nearly available now. We argue the case by presenting higherorder datatypegeneric programs capturing Origami, a small suite of patterns for recursive data structures.

[11] 
Peter Y. H. Wong and Jeremy Gibbons.
A process algebraic approach to workflow verification.
Submitted for publication, 2006.
[ .pdf ]
This paper describes a process algebraic approach to formal verification of workflow processes against abstract specifications. In particular, both specifications and workflow processes are modelled using the process algebra CSP. CSP's behavioural models and their respective refinement relations make it suitable for modelling complex service orchestration and choreography. Moreover, coupled with CSP is an industrial strength automated model checker FDR, which makes CSP very suitable as a process algebra for automatic verification. Twenty control flow workflow patterns introduced by van der Aalst et al. are formalised, and illustrated with a business process scenario.

[12] 
Jeremy Gibbons and Bruno C. d. S. Oliveira.
The essence of the Iterator pattern.
In Conor McBride and Tarmo Uustalu, editors,
MathematicallyStructured Functional Programming, 2006.
[ .pdf ]
The Iterator pattern gives a clean interface for elementbyelement access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various functional iterations model one or other of these, but not both simultaneously. We argue that McBride and Paterson's idioms, and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. We present some axioms for traversal, and illustrate with a simple example, the repmin problem.

[13] 
Jeremy Gibbons.
Fission for program comprehension.
In Tarmo Uustalu, editor, Mathematics of Program Construction,
volume 4014 of Lecture Notes in Computer Science, pages 162179.
SpringerVerlag, 2006.
[ .pdf ]
Fusion is a program transformation that combines adjacent computations, flattening structure and improving efficiency at the cost of clarity. Fission is the same transformation, in reverse: creating structure, ex nihilo. We explore the use of fission for program comprehension, that is, for reconstructing the design of a program from its implementation. We illustrate through rational reconstructions of the designs for three different C programs that count the words in a text file.

[14]  Jeremy Gibbons. Metamorphisms: Streaming representationchangers. Science of Computer Programming, 2006. To appear. [ .pdf ] 
[15] 
Nils Anders Danielsson, Jeremy Gibbons, John Hughes, and Patrik Jansson.
Fast and loose reasoning is morally correct.
In Principles of Programming Languages, January 2006.
[ .pdf ]
We justify reasoning about nontotal (partial) functional languages using methods seemingly only valid for total ones; this permits `fast and loose' reasoning without actually being loose.

[16] 
Jeremy Gibbons.
An unbounded spigot algorithm for the digits of π.
American Mathematical Monthly, 113(4), 2006.
[ .pdf ]
Rabinowitz and Wagon (American Mathematical Monthly 102(3):195203, 1995) present a spigot algorithm for computing the digits of π. A spigot algorithm yields its outputs incrementally, and does not reuse them after producing them. Their algorithm is inherently bounded; it requires a commitment in advance to the number of digits to be computed, and in fact might still produce an incorrect last few digits. We propose two streaming algorithms based on the same characterization of π, with the same incremental characteristics but without requiring the prior bound.

[17]  Jeremy Gibbons, David Lester, and Richard Bird. Enumerating the rationals. Journal of Functional Programming, 16(4), 2006. [ .pdf ] 
[18] 
Jeremy Gibbons and Graham Hutton.
Proof methods for corecursive programs.
Fundamenta Informatica, 66(4), April 2005.
[ .pdf ]
Recursion is a wellknown and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less wellknown, but is increasingly proving to be just as useful. This article is a tutorial on four methods for proving properties of corecursive programs: fixpoint induction, the approximation lemma, coinduction, and fusion.

[19] 
Bruno César dos Santos Oliveira and Jeremy Gibbons.
TypeCase: A design pattern for typeindexed functions.
In Daan Leijen, editor, Haskell Workshop, 2005.
[ .pdf ]
A typeindexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of open typeindexed functions, in which the indexing family can be extended by defining a new type class instance but the collection of functions is fixed. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed typeindexed functions, in which the index family is fixed but the collection of functions is extensible. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that typeindexed functions with typeindexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.

[20] 
Jeremy Gibbons.
Streaming representationchangers.
In Dexter Kozen, editor, Mathematics of Program Construction,
volume 3125 of Lecture Notes in Computer Science, pages 142168, July
2004.
[ http ]
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 unfold after a fold; typically, it will convert from one data representation to another. In general, metamorphisms are less interesting than hylomorphisms: there is no automatic fusion to deforest the intermediate virtual data structure. However, under certain conditions fusion is possible: some of the work of the unfold can be done before all of the work of the fold is complete. This permits streaming metamorphisms, and among other things allows conversion of infinite data representations. We present the theory of metamorphisms and outline some examples.

[21] 
Clare Martin, Jeremy Gibbons, and Ian Bayley.
Disciplined, efficient, generalised folds for nested datatypes.
Formal Aspects of Computing, 16(1):1935, 2004.
[ .pdf ]
Nested (or nonuniform, or nonregular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced generalised folds for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced efficient generalised folds to counter this inefficiency, but did so in a pragmatic way, at the cost of a loss of reasoning power: without categorical or equivalent underpinnings, there are no universal properties for manipulating folds. We combine the efficiency of Hinze's construction with the powerful reasoning tools of Bird and Paterson's.

[22]  Jeremy Gibbons. Patterns in datatypegeneric programming. In Jörg Striegnitz and Kei David, editors, Multiparadigm Programming, volume 27. John von Neumann Institute for Computing (NIC), 2003. First International Workshop on Declarative Programming in the Context of ObjectOriented Languages (DPCOOL). [ .pdf ] 
[23]  Richard Bird and Jeremy Gibbons. Arithmetic coding with folds and unfolds. In Johan Jeuring and Simon Peyton Jones, editors, Advanced Functional Programming 4, volume 2638 of Lecture Notes in Computer Science, pages 126. SpringerVerlag, 2003. [ .pdf ] 
[24]  Roland Backhouse and Jeremy Gibbons, editors. Summer School on Generic Programming, volume 2793 of Lecture Notes in Computer Science. SpringerVerlag, 2003. 
[25]  Jeremy Gibbons and Johan Jeuring, editors. Generic Programming. Kluwer Academic Publishers, 2003. Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloß Dagstuhl, July 2002. ISBN 1402073747. 
[26]  Jeremy Gibbons. Origami programming. In Gibbons and de Moor [27], pages 4160. 
[27]  Jeremy Gibbons and Oege de Moor, editors. The Fun of Programming. Cornerstones in Computing. Palgrave, 2003. ISBN 1403907722. 
[28]  Andrew Simpson, Andrew Martin, Jeremy Gibbons, Jim Davies, and Steve McKeever. On the supervision and assessment of parttime postgraduate software engineering projects. In International Conference on Software Engineering, pages 628633, 2003. [ .pdf ] 
[29]  Andrew Simpson, Andrew Martin, Jeremy Gibbons, Jim Davies, and Steve McKeever. On the supervision and assessment of parttime postgraduate software engineering projects. In Proceedings of the 25th International Conference on Software Engineering, May 310, 2003, Portland, Oregon, USA, pages 628633. IEEE Computer Society, 2003. [ http ] 
[30] 
Jeremy Gibbons.
Towards a colimitbased semantics for visual programming.
In Coordination Models and Languages, volume 2315 of
Lecture Notes in Computer Science, pages 166173, April 2002.
[ .pdf ]
Software architects such as Garlan and Katz promote the separation of computation from coordination. They encourage the study of connectors as firstclass entities, and superposition of connectors onto components as a paradigm for componentoriented programming. We demonstrate that this is a good model for what visual programming tools like IBM's VisualAge actually do. Moreover, Fiadeiro and Maibaum's categorical semantics of parallel programs is applicable to this model, so we can make progress towards a formal semantics of visual programming.

[31] 
Andrew Martin and Jeremy Gibbons.
A monadic interpretation of tactics.
OUCL, February 2002.
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 many applications outside theoremproving activities. The semantics is parametrised by a monad (plus additional structure). By instantiating this in various ways, the core semantics of a number of different tactic languages is obtained.

[32] 
Jeremy Gibbons.
Calculating functional programs.
In Backhouse et al. [34], pages 148203.
[ .pdf ]
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 same way that one calculates numeric values in arithmetic. Many useful theorems for such reasoning derive from an algebraic view of programs, built around datatypes and their operations. Traditional algebraic methods concentrate on initial algebras, constructors, and values; dual coalgebraic methods concentrate on final coalgebras, destructors, and processes. Both methods are elegant and powerful; they deserve to be combined.

[33] 
Richard Bird, Jeremy Gibbons, and Shin Cheng Mu.
Algebraic methods for optimization problems.
In Backhouse et al. [34], pages 281307.
[ .pdf ]
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 a class of optimization problems, deriving efficient functional programs from concise relational specifications.

[34]  Roland Backhouse, Roy Crole, and Jeremy Gibbons, editors. Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of Lecture Notes in Computer Science. SpringerVerlag, 2002. 
[35] 
Clare Martin and Jeremy Gibbons.
On the semantics of nested datatypes.
Information Processing Letters, 80(5):233238, December 2001.
[ .ps.gz ]
Nested (or nonregular or nonuniform) datatypes are recursively defined parameterised datatypes in which the parameter of the datatype changes in the recursive call. The standard semantic definition of recursively defined datatypes is as initial algebras in the category Set of sets and total functions. Bird and Meertens have shown that this theory is inadequate to describe nested datatypes. Instead, one solution proposed there was to define them as initial algebras in the functor category Nat(Set), with objects all endofunctors on Set and arrows all natural transformations between them. We show here that initial algebras are not guaranteed to exist in the functor category itself, but that they do exist in one of its subcategories: the category of all cocontinuous endofunctors and natural transformations. This category is then a suitable semantic domain for nested datatypes, both first order and higherorder.

[36] 
Graham Hutton and Jeremy Gibbons.
The generic approximation lemma.
Information Processing Letters, 79(4):197201, August 2001.
[ .ps.gz ]
The approximation lemma was recently introduced as a simplification of the wellknown 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 to a large class of datatypes, and present a generic approximation lemma that is parametric in the datatype to which it applies. As a useful byproduct, we find that generalising the approximation lemma in this way also simplifies its proof.

[37] 
Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch.
When is a function a fold or an unfold?
Electronic Notes in Theoretical Computer Science, 44(1), April
2001.
Proceedings of Coalgebraic Methods in Computer Science.
[ .ps.gz ]
We give a necessary and sufficient condition for when a settheoretic 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 underlying datatype.

[38] 
Oege de Moor and Jeremy Gibbons.
Pointwise relational programming.
In Algebraic Methodology and Software Technology, volume 1816
of Lecture Notes in Computer Science, pages 371390, May 2000.
[ .ps.gz ]
The pointfree 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 awkward to use: some things are more clearly and simply expressed using variables. The combination of variables and relational combinators such as converse and choice yields a kind of nondeterministic functional programming language. We give a semantics for such a language, and illustrate with an example application.

[39]  Jeremy Gibbons. Lecture notes on algebraic and coalgebraic methods for calculating functional programs. ACMMPC; revision of [43], April 2000. 
[40]  Ian Bayley, Richard Bird, and Jeremy Gibbons. Pattern matching in perfect trees. Oxford University Computing Laboratory, 2000. 
[41] 
Richard Bird, Jeremy Gibbons, and Geraint Jones.
Program optimisation, naturally.
In J. W. Davies, A. W. Roscoe, and J. C. P. Woodcock, editors,
Millenial Perspectives in Computer Science. Palgrave, 2000.
[ .ps.gz ]
It is wellknown that each polymorphic function satisfies a certain equational law, called a naturality condition. Such laws are part and parcel of the basic toolkit for improving the efficiency of functional programs. More rarely, some polymorphic functions also possess a higherorder naturality property. One example is the operation unzip that takes lists of pairs to pairs of lists. Surprisingly, this property can be invoked to improve the asymptotic efficiency of some divideandconquer algorithms from O(n log n) to O(n). The improved algorithms make use of polymorphic recursion, and can be expressed neatly using nested datatypes, so they also serve as evidence of the practical utility of these two concepts.

[42]  Jeremy Gibbons. Generic downwards accumulations. Science of Computer Programming, 37:3765, 2000. [ .ps.gz ] 
[43]  Jeremy Gibbons. Lecture notes on algebraic and coalgebraic methods for calculating functional programs. Estonian Winter School on Computer Science, March 1999. 
[44] 
Oege de Moor and Jeremy Gibbons.
Bridging the algorithm gap: A lineartime functional program for
paragraph formatting.
Science of Computer Programming, 35(1), 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 textbook solution to a problem is not the most efficient possible. However, in presenting the more efficient solution, the algorithm designer will usually omit some of the implementation details, thus creating an algorithm gap between the abstract algorithm and its concrete implementation. This is in contrast to the formal development, which usually proceeds all the way to the complete concrete implementation of the less efficient solution.

[45] 
Jeremy Gibbons and Graham Hutton.
Proof methods for structured corecursive programs.
In Proceedings of 1st Scottish Workshop on Functional
Programming, 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 properties of corecursive programs, including fixpoint induction, the take lemma, and coinduction. However, these methods are all rather lowlevel, in the sense that they do not exploit the common structure that is often present in corecursive definitions. We argue for a more structured approach to proving properties of corecursive programs. In particular, we show that by writing corecursive programs using an operator called unfold that encapsulates a common pattern of corecursive definition, we can then use highlevel algebraic properties of this operator to conduct proofs in a purely calculational style that avoids the use of either induction or coinduction.

[46] 
Jeremy Gibbons.
A pointless derivation of radixsort.
Journal of Functional Programming, 9(3):339346, 1999.
This paper is about pointfree (or `pointless') calculations  calculations performed at the level of function composition instead of that of function application. We address this topic with the help of an example, namely calculating the radixsort algorithm from a more obvious specification of sorting. The message that we hope to send is that pointfree calculations are sometimes surprisingly simpler than the corresponding pointwise calculations.

[47] 
Jeremy Gibbons and Geraint Jones.
The underappreciated unfold.
In Proceedings of the Third ACM SIGPLAN International Conference
on Functional Programming, pages 273279, Baltimore, Maryland, September
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 calculate) a number of algorithms for computing the breadthfirst traversal of a tree. We specify breadthfirst traversal in terms of levelorder traversal, which we characterize first as a fold. The presentation as a fold is simple, but it is inefficient, and removing the inefficiency makes it no longer a fold. We calculate a characterization as an unfold from the characterization as a fold; this unfold is equally clear, but more efficient. We also calculate a characterization of breadthfirst traversal directly as an unfold; this turns out to be the `standard' queuebased algorithm.

[48] 
Jeremy Gibbons.
Polytypic downwards accumulations.
In Johan Jeuring, editor, Proceedings of Mathematics of Program
Construction, volume 1422 of Lecture Notes in Computer Science, pages
207233, Marstrand, Sweden, June 1998. SpringerVerlag.
A downwards accumulation is a higherorder operation that distributes information downwards through a data structure, from the root towards the leaves. The concept was originally introduced in an ad hoc way for just a couple of kinds of tree. We generalize the concept to an arbitrary polynomial datatype; our generalization proceeds via the notion of a path in such a datatype.

[49] 
Jeremy Gibbons.
Structured programming in Java.
SIGPLAN Notices, 33(4):4043, April 1998.
Also in Fintan Culwin, editor, Proceedings of the Second
Conference on Java in the Computing Curriculum, South Bank University,
London.
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 progressing to higherlevel styles such as objectoriented programming. We also argue that, once it has been decided to teach structured programming, Java is a reasonable language to choose for doing so.

[50]  Jeremy Gibbons and Geraint Jones. Against the grain: Lineartime breadthfirst tree algorithms. Oxford Brookes University and Oxford University Computing Laboratory, 1998. 
[51] 
Jeremy Gibbons.
Calculating functional programs.
In Keiichi Nakata, editor, Proceedings of ISRG/SERG Research
Colloquium. School of Computing and Mathematical Sciences, Oxford Brookes
University, November 1997.
Technical Report CMSTR9801.
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 helps calculation. We discuss the ideas behind program calculation, and illustrate with an example (the maximum segment sum problem). We show that calculations are driven by promotion, and that promotion properties arise from universal properties of the data types involved.

[52] 
Jeremy Gibbons.
More on merging and selection.
Technical Report CMSTR9708, School of Computing and Mathematical
Sciences, Oxford Brookes University, October 1997.
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 and y. Representing x and y by trees, Bird derives an algorithm for the problem taking time proportional to the sum of their depths. Bird's derivation is more complicated than necessary. By the simple tactic of delaying a design decision (in this case, the decision to represent the lists as trees) as long as possible, we obtain a much simpler solution.

[53] 
Jeremy Gibbons.
Conditionals in distributive categories.
Technical Report CMSTR9701, School of Computing and Mathematical
Sciences, Oxford Brookes University, January 1997.
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.

[54] 
Jeremy Gibbons.
The Third Homomorphism Theorem.
Journal of Functional Programming, 6(4):657665, 1996.
Earlier version appeared in C.B.Jay, editor, Computing: The
Australian Theory Seminar, Sydney, December 1994, p.6269.
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 necessarily a list homomorphismit can be computed according to any parenthesization of the list.

[55]  Douglas Bridges, Cris Calude, Jeremy Gibbons, Steve Reeves, and Ian Witten, editors. Combinatorics, Complexity and Logic: Proceedings of DMTCS'96, Singapore, 1996. SpringerVerlag. 
[56] 
Jeremy Gibbons.
Deriving tidy drawings of trees.
Journal of Functional Programming, 6(3):535562, 1996.
The treedrawing 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 specification, the starting point for the derivations, consists of a collection of intuitively appealing criteria satisfied by tidy drawings. The derivation shows constructively that these criteria completely determine the drawing. Indeed, there is essentially only one reasonable drawing algorithm satisfying the criteria; its development is almost mechanical.

[57] 
Jeremy Gibbons.
Computing downwards accumulations on trees quickly.
Theoretical Computer Science, 169(1):6780, 1996.
Earlier version appeared in Proceedings of the 16th Australian
Computer Science Conference, Brisbane, 1993.
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' (computable in a functional style in parallel time proportional to the depth of the tree) and `manipulable' (enjoying a number of distributivity properties useful in program construction); we call a downwards pass satisfying these conditions a downwards accumulation. In this paper, we show that these conditions do in fact yield a stronger conclusion: the accumulation can be computed in parallel time proportional to the logarithm of the depth of the tree, on a CREW PRAM machine.

[58] 
Jeremy Gibbons and Keith Wansbrough.
Tracing lazy functional languages.
In Michael E. Houle and Peter Eades, editors, Computing: The
Australasian Theory Seminar, pages 1120, Melbourne, January 1996.
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the callbyneed lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional languages. In particular, it allows a onedimensional textual representation of terms, rather than requiring a twodimensional graphical representation using arrows. We describe a program LetTrace, implemented in Gofer and tracing lazy evaluation of a subset of Gofer.

[59] 
Jeremy Gibbons.
Dotted and dashed lines in Metafont.
In Robin Fairbairns, editor, Proceedings of the 1995 Annual
Meeting. T_{E}X Users' Group, 1995.
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 here can be used for both Metafont and Metapost.

[60] 
Jeremy Gibbons.
An initialalgebra approach to directed acyclic graphs.
In Bernhard Möller, editor, Mathematics of Program
Construction, volume 947 of Lecture Notes in Computer Science, pages
282303. SpringerVerlag, 1995.
The initialalgebra 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 same object. The recursive decomposition of objects of the datatype leads directly to a recursive pattern of computation on those objects, which is very helpful for both functional and parallel programming.

[61] 
Jeremy Gibbons.
An introduction to the BirdMeertens Formalism.
In Steve Reeves, editor, Proceedings of the First New Zealand
Formal Program Development Colloquium, pages 112, Hamilton, November 1994.
The BirdMeertens Formalism, or `Squiggol', is a calculus for the construction of programs from their specifications by a process of equational reasoning. Developments are directed by considerations of data, as opposed to program, structure.

[62] 
Jeremy Gibbons, Wentong Cai, and David Skillicorn.
Efficient parallel algorithms for tree accumulations.
Science of Computer Programming, 23:118, 1994.
Accumulations are higherorder operations on structured objects; they leave the shape of an object unchanged, but replace elements of that object with accumulated information about other elements. Upwards and downwards accumulations on trees are two such operations; they form the basis of many tree algorithms. We present two EREW PRAM algorithms for computing accumulations on trees taking O(logn) time on O(n/logn) processors, which is optimal.

[63]  Jeremy Gibbons. How to derive tidy drawings of trees. In C. Calude, M. J. J. Lennon, and H. Maurer, editors, Proceedings of Salodays in Auckland, pages 5373, Department of Computer Science, University of Auckland, 1994. Also in Proceedings of First New Zealand Formal Program Development Colloquium, p.105126. 
[64]  Jeremy Gibbons. Algebraic models of graphs. IFIP Working Group 2.1 working paper 722 REN7, January 1994. 
[65] 
Geraint Jones and Jeremy Gibbons.
Lineartime breadthfirst tree algorithms: An exercise in the
arithmetic of folds and zips.
Computer Science Report No.71, Dept of Computer Science, University
of Auckland, May 1993.
Also IFIP Working Group 2.1 working paper 705WIN2.
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 lineartime breadthfirst tree traversal algorithm, and of a subtle and efficient breadthfirst tree labelling algorithm.

[66] 
Jeremy Gibbons.
Computing downwards accumulations on trees quickly.
In Gopal Gupta, George Mohay, and Rodney Topor, editors, 16th
Australian Computer Science Conference, pages 685691, Brisbane, February
1993.
Revised version [57].
Downwards accumulations on binary trees are essentially functions which pass information down a tree. Under certain conditions, these accumulations are both `efficient' (computable in a functional style in parallel time proportional to the depth of the tree) and `manipulable'. In this paper, we show that these conditions do in fact yield a stronger conclusion: the accumulation can be computed in parallel time proportional to the logarithm of the depth of the tree, on a Crew Pram machine.

[67] 
Jeremy Gibbons.
Formal methods: Why should I care? The development of the T800
Transputer floatingpoint unit.
In John Hosking, editor, Proceedings of the 13th New Zealand
Computer Society Conference, pages 207217, 1993.
The term `formal methods' is a general term for precise mathematicallybased techniques used in the development of computer systems, both hardware and software. This paper discusses formal methods in general, and in particular describes their successful role in specifying, constructing and proving correct the floatingpoint unit of the Inmos T800 transputer chip.

[68] 
Jeremy Gibbons.
Upwards and downwards accumulations on trees.
In R. S. Bird, C. C. Morgan, and J. C. P. Woodcock, editors,
Mathematics of Program Construction, volume 669 of Lecture Notes in
Computer Science, pages 122138. SpringerVerlag, 1993.
A revised version appears in the Proceedings of the Massey Functional
Programming Workshop, 1992.
An accumulation is a higherorder operation over structured objects of some type; it leaves the shape of an object unchanged, but replaces each element of that object with some accumulated information about the other elements. Upwards and downwards accumulations on trees are two instances of this scheme; they replace each element of a tree with some functionin fact, some homomorphismof that element's descendants and of its ancestors, respectively. These two operations can be thought of as passing information up and down the tree.

[69] 
Jeremy Gibbons.
Algebras for Tree Algorithms.
D.Phil.thesis, Programming Research Group, Oxford University,
1991.
Available as Technical Monograph PRG94. ISBN 0902928724.
This thesis presents an investigation into the properties of various algebras of trees. In particular, we study the influence that the structure of a tree algebra has on the solution of algorithmic problems about trees in that algebra. The investigation is conducted within the framework provided by the BirdMeertens formalism, a calculus for the construction of programs by equational reasoning from their specifications.

[70]  Richard S. Bird, Jeremy Gibbons, and Geraint Jones. Formal derivation of a pattern matching algorithm. Science of Computer Programming, 12(2):93104, July 1989. 
[71] 
Jeremy Gibbons.
A new view of binary trees.
Transferral dissertation, Programming Research Group, Oxford
University, 1988.
Abstract appears in the Bulletin of the EATCS, number 39, p. 214.
We present a new formalism of labelled binary trees, using two partial binary constructors instead of the usual total ternary constructor. This formalism is complemented by some higherorder operators, encapsulating common patterns of computation on trees. We explore their use by deriving solutions to a couple of algorithmic problems on trees.

This file has been generated by bibtex2html 1.85.