@unpublished{Gibbons&Paterson2008:Parametric,
abstract = "Datatype-generic programs are programs that are parametrized by a datatype or type functor: whereas polymorphic programs abstract from the "integers" in "lists of integers", datatype-generic programs abstract from the "lists of". There are two main styles of datatype-generic programming: the Algebra of Programming approach, characterized by structured recursion operators arising from initial algebras and final coalgebras, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of higher-order naturality, relating the behaviours of generic functions at different types; in contrast, the latter is more ad hoc, with no coherence required or provided between the various clauses of a definition. Moreover, the naturality properties arise "for free", simply from the parametrized types of the generic functions: we present a higher-order parametricity theorem for datatype-generic operators.",
author = "Jeremy Gibbons and Ross Paterson",
note = "Submitted for publication",
title = "Parametric Datatype-Genericity",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/parametric.pdf",
year = "2008",
}
@inproceedings{Wong&Gibbons2008:Process,
abstract = "Business Process Modelling Notation (BPMN), developed by the Business Process Management Initiative (BPMI), intends to bridge the gap between business process design and implementation. However, the specification of the notation does not include a formal semantics. This paper shows how a subset of the BPMN can be given a process semantics in Communicating Sequential Processes. Such a semantics allows developers to formally analyse and compare BPMN diagrams. A realistic example of a complex business process is included.",
address = "Kitakyushu, Japan",
author = "Peter Wong and Jeremy Gibbons",
booktitle = "International Conference on Formal Engineering Methods",
month = "September",
title = "A Process Semantics for BPMN",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/bpmn-csp.pdf",
year = "2008",
}
@inproceedings{Oliveira&Gibbons2008:Scala,
abstract = "Datatype-generic programming involves parametrization by the shape of data, in the form of type constructors such as "list of". Most approaches to datatype-generic programming are developed in the lazy functional programming language Haskell. We argue that the functional object-oriented language Scala is in many ways a better setting. Not only does Scala provide equivalents of all the necessary functional programming features (such parametric polymorphism, higher-order functions, higher-kinded type operations,and type- and constructor-classes), but it also provides the most useful features of object-oriented languages (such as subtyping,overriding, traditional single inheritance, and multiple inheritance in the form of traits). We show how this combination of features benefits datatype-generic programming, using three different approaches as illustrations.",
address = "Victoria, BC",
author = "Bruno Oliveira and Jeremy Gibbons",
booktitle = "Workshop on Generic Programming",
editor = "Ralf Hinze",
month = "Sep",
title = "Scala for Generic Programmers",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/scalagp.pdf",
year = "2008",
}
@inproceedings{Smith&Gibbons2008:Unifying,
abstract = "We present a Unifying Theories of Programming (UTP) model of locations, where a location is either shareable or containable depending on whether its value can be dereferenced by a pointer. Our model of locations is similar to previous work on pointers within the UTP; the main difference is that the previous work on pointers only modelled shareable locations. We explain why containable locations are useful, present an outline of our UTP model, and compare it to the existing UTP work. We hope to convince the reader that a general model of pointers within the UTP ought to be able to represent both shareable and containable locations. Here, the contents of contained locations need to be duplicated, whereas the contents of shared locations are referenced.",
address = "Dublin",
author = "Michael Anthony Smith and Jeremy Gibbons",
booktitle = "Unifying Theories of Programming",
editor = "Andrew Butterfield",
month = "Sep",
title = "Unifying Theories of Locations",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/utl.pdf",
year = "2008",
}
@inproceedings{Wong&Gibbons2008:Relative,
abstract = "We describe a relative-timed semantic model for Business Process Modelling Notation (BPMN). We define the semantics in the language of Communicating Sequential Processes (CSP). This model augments our untimed model by introducing the notion of relative time in the form of delays chosen non-deterministically from a range. By using CSP as the semantic domain, we exploit its refinement to show some properties relating the timed semantics and BPMN's untimed process semantics. Our timed semantics allows behavioural properties of BPMN diagrams to be mechanically verified via automatic model-checking provided by the FDR tool.",
address = "Zurich",
author = "Peter Wong and Jeremy Gibbons",
booktitle = "Foundations of Coordination Languages and Software Architectures (FOCLASA)",
month = "July",
title = "A Relative Timed Semantics for BPMN",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/relative.pdf",
year = "2008",
}
@article{Gibbons&Oliveira2008:Essence,
abstract = "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 existing functional iterations model one or other of these, but not both simultaneously. We argue that McBride and Paterson's applicative functors, 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 wordcount problem.",
author = "Jeremy Gibbons and Bruno C\'esar dos Santos Oliveira",
journal = "Journal of Functional Programming",
note = "Revised version of \cite{Gibbons&Oliveira2006:Essence}",
title = "The Essence of the Iterator Pattern",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf",
year = "2008",
}
@inproceedings{Zang*2008:WSRF,
abstract = "The CancerGrid consortium is developing open-standards cancer informatics to address the challenges posed by modern cancer clinical trials. This paper presents the service-oriented software paradigm implemented in CancerGrid to derive clinical trial information management systems for collaborative cancer research across multiple institutions. Our proposal is founded on a combination of a clinical trial (meta)model and WSRF (Web Services Resource Framework), and is currently being evaluated for use in early phase trials. Although primarily targeted at cancer research, our approach is readily applicable to other areas for which a similar information model is available.",
author = "Tianyi Zang and Radu Calinescu and Steve Harris and Andrew Tsui and Marta Kwiatkowska and Jeremy Gibbons and Jim Davies and Peter Maccallum and Carlos Caldas",
booktitle = "8th IEEE International Symposium on Cluster Computing (CCGrid)",
title = "WSRF-Based Modeling of Clinical Trial Information for Collaborative Cancer Research",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/wsrfmodeling.pdf",
year = "2008",
}
@inproceedings{Gibbons2008:Unfolding,
abstract = "Abstract datatypes — with public interfaces hiding private implementations — represent a form of codata rather than ordinary data, and so proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with the solution to a problem in the recent literature.",
author = "Jeremy Gibbons",
booktitle = "Mathematics of Program Construction",
month = "jul",
title = "Unfolding Abstract Datatypes",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/adt.pdf",
year = "2008",
}
@inproceedings{Wong&Gibbons2008:Verifying,
abstract = "We describe a process-algebraic approach to verifying process interactions for business collaboration described in Business Process Modelling Notation. We first overview our process semantics for BPMN in the language of 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.",
author = "Peter Wong and Jeremy Gibbons",
booktitle = "8th International Conference on Quality Software (QSIC)",
note = "Earlier versions of this paper were presented at the 2nd European Young Researchers Workshop on Service Oriented Computing, Leicester, United Kingdom, June 2007, and 3rd International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord'07), Paphos, Cyprus, June 2007",
title = "Verifying Business Process Compatibility",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/compatibility.pdf",
year = "2008",
}
@inproceedings{Wong&Gibbons2008:Specifying,
abstract = "We describe a graphical approach to formally specifying temporally ordered activity routines designed for calendar scheduling. We introduce a workflow model OWorkflow, for constructing specifications of long running empirical studies such as clinical trials in which observations for gathering data are performed at strict specific times. These observations, either manually performed or automated, are often interleaved with scientific procedures, and their descriptions are recorded in a calendar for scheduling and monitoring to ensure each observation is carried out correctly at a specific time. We also describe a bidirectional transformation between OWorkflow and a subset of Business Process Modelling Notation (BPMN), by which graphical specification, simulation, automation and formalisation are made possible.",
author = "Peter Y. H. Wong and Jeremy Gibbons",
booktitle = "International Conference on Model Transformations (ICMT)",
title = "On Specifying and Visualising Long-Running Empirical Studies",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/longrunning.pdf",
year = "2008",
}
@inproceedings{Oliveira*2008:Visitor,
abstract = "The Visitor design pattern shows how to separate the structure of an object hierarchy from the behaviour of traversals over that hierarchy. The pattern is very flexible; this very flexibility makes it difficult to capture the pattern as anything more formal than prose, pictures and prototypes. We show how to capture the essence of the Visitor pattern as a reusable software library, by using advanced type system features appearing in modern object-oriented languages such as Scala. We preserve type-safety statically: no reflection or similar mechanisms are used. The library is generic, in two senses: not only is it parametrised by both the return type and the shape of the object hierarchy, but also it allows a number of implementation choices (internal versus external control, imperative versus functional behaviour,orthogonal aspects such as tracing and memoisation) to be specified by parameters rather than fixed in early design decisions. Finally, we propose a generalised datatype-like notation, on top of our visitor library: this provides a convenient functional decomposition style in object-oriented languages.",
author = "Bruno C. d. S. Oliveira and Meng Wang and Jeremy Gibbons",
booktitle = "Object-Oriented Programming: Systems, Languages, Applications (OOPSLA)",
title = "The Visitor Pattern as a Reusable, Generic, Type-Safe Component",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/visitor.pdf",
year = "2008",
}
@inproceedings{DBLP:conf/icegov/CrichtonDGHS07,
abstract = "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 how metadata standards and repositories can be used to establish and maintain such an understanding, and how they can be used in the automatic generation and instantiation of components and services. It includes an account of a successful implementation at an international level, and a brief review of related approaches.",
author = "Charles Crichton and Jim Davies and Jeremy Gibbons and Steve Harris and Aadya Shukla",
booktitle = "First International Conference on Theory and Practice of Electronic Governance (ICEGOV) 2007",
doi = "10.1145/1328057.1328066",
editor = "Theresa Pardo and Tomasz Janowski",
month = "dec",
pages = "30--39",
publisher = "ACM",
title = "Semantic Frameworks for e-Government",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/icegov.pdf",
year = "2007",
}
Warning - the bibtex entry below may be invalid:
Missing 'note' field
@unpublished{Gibbons2007:Commercial,
abstract = "The goal of the Commercial Users of Functional Programming series of workshops is "to build a community for users of functional programming languages and technology". The fourth workshop in the series took place in Freiburg, Germany on 4th October 2007, colocated as usual with the International Conference on Functional Programming. The workshop is flourishing, having grown from an intimate gathering of 25 people in Snowbird in 2004, through 40 in Tallinn in 2005 and 57 in Portland in 2006, to 104 registered participants (and more than a handful of casual observers) this time. For the first time this year, the organisers had the encouraging dilemma of receiving more offers of presentations than would fit in the available time. The eventual schedule included an invited talk by Xavier Leroy, eleven contributed presentations, and an energetic concluding discussion.",
author = "Jeremy Gibbons",
month = "December",
title = "Report on Fourth Workshop on Commercial Users of Functional Programming",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/cufp2007.pdf",
year = "2007",
}
@article{Gibbons2005:Metamorphisms,
abstract = "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.",
author = "Jeremy Gibbons",
journal = "Science of Computer Programming",
pages = "108-139",
title = "Metamorphisms: Streaming Representation-Changers",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/metamorphisms-scp.pdf",
volume = "65",
year = "2007",
}
@inproceedings{Wong&Gibbons2007:ProcessAlgebraic,
abstract = "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.",
author = "Peter Y. H. Wong and Jeremy Gibbons",
booktitle = "Software Composition",
title = "A Process-Algebraic Approach to Workflow Specification and Refinement",
url = "http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/sc2007.pdf",
year = "2007",
}
@inproceedings{Gibbons*2007:Generic,
abstract = "The EPSRC-funded \emph{Generic and Indexed Programming} project will explore the interaction between \emph{datatype-generic programming} (DGP) ---~programs parametrized by the shape of their data~--- and \emph{indexed programming} (IP) ---~lightweight dependently-typed programming, with programs indexed by type-level representations of properties. Integrating these two notions will provide new ways for programmers to \emph{capture abstractions}.",
author = "Jeremy Gibbons and Meng Wang and Bruno C\'esar dos Santos Oliveira",
booktitle = "Trends in Functional Programming",
editor = "Marco Morazan",
title = "Generic and Indexed Programming",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/gip.pdf",
year = "2007",
}
@proceedings{Backhouse*2007:Datatype,
abstract = "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 can be envisaged in a programming language range from simple values, like integers and floating-point numbers, through structured values, types and classes, to kinds (the type of types and/or classes). Datatype-generic programming is about parametrising programs by the structure of the data that they manipulate, exploiting that structure when it is relevant and ignoring it when it is not. Programming languages most commonly used at the present time do not provide effective mechanisms for documenting and implementing datatype genericity. This volume is a contribution towards improving the state of the art. 
",
booktitle = "Spring School on Datatype-Generic Programming",
editor = "Roland Backhouse and Jeremy Gibbons and Ralf Hinze and Johan Jeuring",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Spring School on Datatype-Generic Programming",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/ssdgp-preface.pdf",
volume = "4719",
year = "2007",
}
@inproceedings{Gibbons2007:Datatype,
abstract = "\emph{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: \emph{parametric polymorphism}, \emph{data abstraction}, \emph{meta-programming}, and so on. We use it to mean polytypism, that is, parametrization by the \emph{shape} of data structures rather than their contents. To avoid confusion with other uses, we have coined the qualified term \emph{datatype-generic programming} for this purpose. In these lecture notes, we expand on the definition of datatype-generic programming, and present some examples of datatype-generic programs. We also explore the connection with \emph{design patterns} in object-oriented programming; in particular, we argue that certain design patterns are just higher-order datatype-generic programs.",
author = "Jeremy Gibbons",
booktitle = "Spring School on Datatype-Generic Programming",
editor = "Roland Backhouse and Jeremy Gibbons and Ralf Hinze and Johan Jeuring",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Datatype-Generic Programming",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/dgp.pdf",
volume = "4719",
year = "2007",
}
@proceedings{Davies&Gibbons2007:Integrated,
abstract = "The design and analysis of computing systems presents a significant challenge: systems need to be understood at many different levels of abstraction, and examined from many different perspectives. Formal methods?languages, tools, and techniques with a sound, mathematical basis?can be used to develop a thorough understanding, and to support rigorous examination. Further research into effective integration is required if these methods are to have a significant impact outside academia. The Integrated Formal Methods (IFM) series of conferences seeks to promote that research, to bring together the researchers carrying it out, and to disseminate the results of that research among the wider academic and industrial community. Earlier meetings in the series were held at: York (1999); Dagstuhl (2000); Turku (2002); Kent (2004); Eindhoven (2005). IFM 2007 is the largest to date, with 32 technical papers (from 85 submissions), 3 invited talks, 3 workshops, and a tutorial. The success of the series reflects the enthusiasm and efforts of the IFM community, and the organisers would like to thank the speakers, the committee, and the reviewers for their contributions. 
",
booktitle = "Integrated Formal Methods",
editor = "Jim Davies and Jeremy Gibbons",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Integrated Formal Methods",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/ifm2007-preface.pdf",
volume = "4591",
year = "2007",
}
@inproceedings{Smith&Gibbons2007:Unifying,
abstract = "We present an approach to modelling Abadi–Cardelli-style object calculi as UTP designs. Here we provide a core object calculus with an operational small-step 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 object-based and class-based languages.",
author = "Michael Anthony Smith and Jeremy Gibbons",
booktitle = "Integrated Formal Methods",
editor = "Jim Davies and Jeremy Gibbons",
pages = "599-618",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Unifying Theories of Objects",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/uto.pdf",
volume = "4591",
year = "2007",
}
@inproceedings{Calinescu*2007:Model,
abstract = "It is a common phenomenon for research projects to collect and analyse valuable data using ad-hoc information systems. These costly-to-build systems are often composed of incompatible variants of the same modules, and record data in ways that prevent any meaningful result analysis across similar projects. We present a framework that uses a combination of formal methods, model-driven development and service-oriented architecture (SOA) technologies to automate the generation of data management systems for cancer clinical trial research, an area particularly affected by these problems. The SOA solution generated by the framework is based on an information model of a cancer clinical trial, and comprises components for both the collection and analysis of cancer research data, within and across clinical trial boundaries. While primarily targeted at cancer research, our approach is readily applicable to other areas for which a similar information model is available.",
author = "Radu Calinescu and Steve Harris and Jeremy Gibbons and Jim Davies and Igor Toujilov and Sylvia Nagl",
booktitle = "Software Engineering and Formal Methods",
month = "sep",
title = "Model-Driven Architecture for Cancer Research",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/cgmda.pdf",
year = "2007",
}
@article{Gibbons*2006:Enumerating,
abstract = "We present a series of programs for enumerating the rational numbers without duplication, drawing on some elegant results of Neil Calkin, Herbert Wilf and Moshe Newman.",
author = "Jeremy Gibbons and David Lester and Richard Bird",
journal = "Journal of Functional Programming",
number = "4",
title = "Enumerating the Rationals",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/rationals.pdf",
volume = "16",
year = "2006",
}
@article{Gibbons2006:Spigot,
abstract = "Rabinowitz and Wagon (\textit{American Mathematical Monthly} 102(3):195--203, 1995) present a \emph{spigot algorithm} for computing the digits of $\pi$. A spigot algorithm yields its outputs incrementally, and does not reuse them after producing them. Their algorithm is inherently \emph{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 \emph{streaming algorithms} based on the same characterization of $\pi$, with the same incremental characteristics but without requiring the prior bound.",
author = "Jeremy Gibbons",
journal = "American Mathematical Monthly",
number = "4",
pages = "318-328",
title = "An Unbounded Spigot Algorithm for the Digits of $\pi$",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/spigot.pdf",
volume = "113",
year = "2006",
}
@inproceedings{Danielsson*2006:Fast,
abstract = "We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits `fast and loose' reasoning without actually being loose. \par Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values and lifted types, including lifted function spaces. A partial equivalence relation is then defined, the domain of which is the total subset of the partial language. It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the partial equivalence relation gives rise to a bicartesian closed category, which can be used to reason about values in the domain of the relation.",
author = "Nils Anders Danielsson and Jeremy Gibbons and John Hughes and Patrik Jansson",
booktitle = "Principles of Programming Languages",
month = "jan",
pages = "206-217",
title = "Fast and Loose Reasoning is Morally Correct",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf",
year = "2006",
}
@inproceedings{Gibbons2006:Fission,
abstract = "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.",
author = "Jeremy Gibbons",
booktitle = "Mathematics of Program Construction",
editor = "Tarmo Uustalu",
pages = "162-179",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Fission for Program Comprehension",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/fission.pdf",
volume = "4014",
year = "2006",
}
@inproceedings{Gibbons2006:Design,
abstract = "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 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 \emph{higher-order} and \emph{datatype-generic} constructs; these features are already or nearly available now. We argue the case by presenting higher-order datatype-generic programs capturing Origami, a small suite of patterns for recursive data structures.",
author = "Jeremy Gibbons",
booktitle = "Workshop on Generic Programming",
editor = "Ralf Hinze",
month = "sep",
title = "Design Patterns as Higher-Order Datatype-Generic Programs",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/hodgp.pdf",
year = "2006",
}
@inproceedings{Gibbons&Oliveira2006:Essence,
abstract = "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 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.",
author = "Jeremy Gibbons and Bruno C\'esar dos Santos Oliveira",
booktitle = "Mathematically-Structured Functional Programming",
editor = "Conor McBride and Tarmo Uustalu",
note = "Superseded by \cite{Gibbons&Oliveira2008:Essence}",
title = "The Essence of the Iterator Pattern",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/iterator-msfp.pdf",
year = "2006",
}
@inproceedings{Calinescu*2006:Cross,
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 software engineers from leading UK institutions, is developing open-standards cancer informatics addressing this challenge. The CancerGrid solution involves the representation of a widely accepted clinical trials model in controlled vocabulary and common data elements (CDEs) as the enabling factor for cancer data sharing. This paper describes a cancer data query system that supports data sharing across CancerGrid-compliant clinical trial boundaries. The formal specification of the query system allows the model-driven development of a flexible, web-based interface that cancer researchers with limited IT experience can use to identify and query common data across multiple clinical trials.",
author = "Radu Calinescu and Steve Harris and Jeremy Gibbons and Jim Davies",
booktitle = "International Joint Conferences on Computer, Information and Systems Sciences and Engineering (CISSE)",
month = "dec",
title = "Cross-Trial Query System for Cancer Clinical Trials",
url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/crosstrial.pdf",
year = "2006",
}
@article{Gibbons&Hutton2005:Proof,
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 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.",
author = "Jeremy Gibbons and Graham Hutton",
journal = "Fundamenta Informaticae",
month = "April/May",
number = "4",
pages = "353-366",
title = "Proof Methods for Corecursive Programs",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/corecursive.pdf",
volume = "66",
year = "2005",
}
@inproceedings{Gibbons2005:DesignECOOP,
abstract = "The aim of this tutorial is to draw together ideas from the Design Patterns community (the Gang of Four: Gamma, Helm, Johnson, Vlissides) and the Functional Programming world (eg Bird, Meertens, Hughes). In particular, the thesis is that whereas design patterns must be expressed extra-linguistically (as prose, diagrams, examples) in object-oriented languages, they may be captured directly as abstractions using higher-order operators in functional programming languages. Therefore, they may be reasoned about, type-checked, applied and reused, just as any other abstractions may be. We argue this case by developing the idea of higher-order operators, specifically for capturing patterns of computation in programs. We then bring this around to show how the intentions behind a number of the Gang of Four patterns---such as Composite, Visitor, Iterator, and Builder---have higher-order operators as their analogues in functional languages.",
address = "Glasgow",
author = "Jeremy Gibbons",
booktitle = "European Conference on Object-Oriented Programming",
month = "jul",
note = "Later version appears as \cite{Gibbons2005:DesignOOPSLA}",
title = "Design Patterns as Higher-Order Datatype-Generic Programs",
url = "http://2005.ecoop.org/8.html",
year = "2005",
}
@inproceedings{Gibbons2005:DesignOOPSLA,
abstract = "The purpose of this tutorial is to draw together ideas from the Design Patterns community (the Gang of Four: Gamma, Helm, Johnson, Vlissides) and the Functional Programming world (eg Bird, Meertens, Hughes). In particular, the thesis is that whereas design patterns must be expressed extra-linguistically (as prose, diagrams, examples) in object-oriented languages, they may be captured directly as abstractions using higher-order operators in functional programming languages. Therefore, they may be reasoned about, type-checked, applied and reused, just as any other abstractions may be. \par We argue this case by developing the idea of higher-order operators, specifically for capturing patterns of computation in programs. We then build on this to show how the intentions behind a number of the Gang of Four patterns---such as Composite, Visitor, Iterator, and Builder---have higher-order operators as their analogues in functional languages. Specifically, the structure of these patterns is determined essentially by the structure of the data involved, and they can be captured as generic programs parametrized by that datatype. \par The aim is to give greater insight into and understanding of already-familiar patterns.",
address = "San Diego",
author = "Jeremy Gibbons",
booktitle = "Object-Oriented Programming: Systems, Languages, Applications",
month = "oct",
note = "A revision of \cite{Gibbons2005:DesignECOOP}",
title = "Design Patterns as Higher-Order Datatype-Generic Programs",
url = "http://www.oopsla.org/2005/ShowEvent.do?id=121",
year = "2005",
}
@inproceedings{Oliveira&Gibbons2005:TypeCase,
abstract = "A \emph{type-indexed function} is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of \emph{open type-indexed 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 \emph{TypeCase}: a design pattern that allows the definition of \emph{closed type-indexed 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 \emph{design pattern}. Furthermore, we show that \emph{type-indexed functions} with \emph{type-indexed types}, and consequently \emph{generic functions} with \emph{generic types}, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.",
author = "Bruno C\'esar dos Santos Oliveira and Jeremy Gibbons",
booktitle = "Haskell Workshop",
editor = "Daan Leijen",
pages = "98-109",
title = "TypeCase: A Design Pattern for Type-Indexed Functions",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/typecase.pdf",
year = "2005",
}
@article{Martin*2004:Disciplined,
abstract = "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 introduced \emph{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 \emph{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.",
author = "Clare Martin and Jeremy Gibbons and Ian Bayley",
journal = "Formal Aspects of Computing",
number = "1",
pages = "19-35",
title = "Disciplined, efficient, generalised folds for nested datatypes",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/efolds.pdf",
volume = "16",
year = "2004",
}
@inproceedings{Gibbons2004:Streaming,
abstract = "\emph{Unfolds} generate data structures, and \emph{folds} consume them. A \emph{hylomorphism} is a fold after an unfold, generating then consuming a \emph{virtual data structure}. A \emph{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 \emph{fusion} to \emph{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 \emph{streaming metamorphisms}, and among other things allows conversion of \emph{infinite data representations}. We present the theory of metamorphisms and outline some examples.",
author = "Jeremy Gibbons",
booktitle = "Mathematics of Program Construction",
editor = "Dexter Kozen",
month = "jul",
note = "\url{http://www.springerlink.com/index/LHQ73WU5GU686976}",
pages = "142-168",
series = "Lecture Notes in Computer Science",
title = "Streaming Representation-Changers",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/metamorphisms-mpc.pdf",
volume = "3125",
year = "2004",
}
@book{Backhouse&Gibbons2003:Summer,
abstract = "Generic programming is about making programming more effective by making it more general. This volume is about a novel form of genericity in programs, based on parameterizing programs by the structure of the data they manipulate. The material is based on lectures presented at a summer school on Generic Programming held at the University of Oxford in August 2002. 
",
booktitle = "Summer School on Generic Programming",
editor = "Roland Backhouse and Jeremy Gibbons",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Summer School on Generic Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/ssgp-toc.pdf",
volume = "2793",
year = "2003",
}
@inproceedings{Simpson*2002:Supervision,
abstract = "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 experience, and the educational issues raised, in the context of existing literature---much of which is focussed upon the experience of full-time, undergraduate students. The importance of these issues will increase with the popularity of part-time study at a postgraduate level; the paper presents a set of guidelines for project supervision and assessment.",
author = "Andrew Simpson and Andrew Martin and Jeremy Gibbons and Jim Davies and Steve McKeever",
booktitle = "International Conference on Software Engineering",
pages = "628-633",
title = "On The Supervision and Assessment Of Part-Time Postgraduate Software Engineering Projects",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/softeng-projects.pdf",
year = "2003",
}
@proceedings{Gibbons&Jeuring2003:Generic,
abstract = "Generic programming techniques have always been of interest, both to practitioners and to theoreticians, but only recently have generic programming techniques become a specific focus of research in the functional and object-oriented programming language communities. The IFIP TC2 Working Conference on Generic Programming, held at Schloss Dagstuhl, Germany, on 11th and 12th July 2002, brought together leading researchers in generic programming from around the world, and featured papers capturing the state of the art in this important emerging area. The conference was sponsored by IFIP Technical Committee 2, and organized in cooperation with Working Group 2.1 on Algorithmic Languages and Calculi. This book contains revised versions of the papers that were presented at the conference. 
",
booktitle = "Generic Programming",
editor = "Jeremy Gibbons and Johan Jeuring",
note = "Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schlo\ss{} Dagstuhl, July 2002. ISBN 1-4020-7374-7",
publisher = "Kluwer Academic Publishers",
title = "Generic Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/wcgp-preface.pdf",
year = "2003",
}
@book{Gibbons&deMoor2003:Fun,
abstract = "Functional programming has come of age: it is now a standard course in any computer science curriculum. Ideas that were first developed in the laboratory environment of functional programming have proved their values in wider settings, such as generic Java and XML. The time is ripe, therefore, to teach a second course on functional programming, delving deeper into the subject. This book is the text for such a course. The emphasis is on the fun of programming in a modern, well designed programming language such as Haskell. There are chapters that focus on applications, in particular pretty printing, musical composition, hardware description, and graphical design. These applications are interspersed with chapters on techniques, such as the design of efficient data structures, interpreters for other languages, program testing and optimisation. These topics are of interest to every aspiring programmer, not just to those who choose to work in a functional language. Haskell just happens to be a very convenient vehicle for expressing the ideas, and the theme of functional programming as a lingua franca to communicate ideas runs throughout the book. 
",
booktitle = "The Fun of Programming",
editor = "Jeremy Gibbons and Oege de Moor",
note = "ISBN 1-4039-0772-2",
publisher = "Palgrave",
series = "Cornerstones in Computing",
title = "The Fun of Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fop-preface.pdf",
year = "2003",
}
@incollection{Gibbons2003:Origami,
abstract = "One style of functional programming is based purely on recursive equations. Such equations are easy to explain, and adequate for any computational purpose, but hard to use well as programs get bigger and more complicated. In a sense, recursive equations are the `assembly language' of functional programming, and direct recursion the \emph{goto}. As computer scientists discovered in the 1960s with structured programming, it is better to identify common patterns of use of such too-powerful tools, and capture these patterns as new constructions and abstractions. In functional programming, in contrast to imperative programming, we can often express the new constructions as higher-order operations within the language, whereas the move from unstructured to structured programming entailed the development of new languages. \par In this chapter we will look at folds and unfolds as abstractions. In a precise technical sense, folds and unfolds are the natural patterns of computation over recursive datatypes; unfolds generate data structures and folds consume them. Functional programmers are very familiar with the \emph{foldr} function on lists, and its directional dual \emph{foldl}; they are gradually coming to terms with the generalisation to folds on other datatypes. The computational duals, unfolds, are still rather unfamiliar; we hope to show here that they are no more complicated than, and just as useful as, folds, and to promote a style of programming based on these and similar recursion patterns.",
author = "Jeremy Gibbons",
booktitle = "The Fun of Programming",
editor = "Jeremy Gibbons and Oege de Moor",
isbn = "1-4039-0772-2",
pages = "41-60",
publisher = "Palgrave",
series = "Cornerstones in Computing",
title = "Origami Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/origami.pdf",
year = "2003",
}
@inproceedings{Bird&Gibbons2003:Arithmetic,
abstract = "Arithmetic coding is a method for data compression. It produces a theoretically optimal compression under much weaker assumptions than Huffman and Shannon-Fano, and can compress within one bit of the limit imposed by Shannon's Noiseless Coding Theorem. Earlier presentations provided little in the way of proof of why the various steps in the encoding process were correct, particularly when it came to the specification of precisely what problem the implementation solved, and the details of why the inverse operation of decoding was correct. Our aim in these lectures is to provide a formal derivation of basic algorithms for coding and decoding. Our development makes heavy use of the algebraic laws of folds and unfolds. One novel result concerns a new pattern of computation, which we call \emph{streaming}, whereby elements of an output list are produced as soon as they are determined (and which has nothing to do with lazy evaluation).",
author = "Richard Bird and Jeremy Gibbons",
booktitle = "Advanced Functional Programming 4",
editor = "Johan Jeuring and Peyton Jones, Simon",
note = "Code available at \url{http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/arith.zip}",
pages = "1-26",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Arithmetic Coding with Folds and Unfolds",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/arith.pdf",
volume = "2638",
year = "2003",
}
@inproceedings{Gibbons2003:Patterns,
abstract = "\emph{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 Template Library. \emph{Datatype-generic programming} is another instance, in which the parameters take the form of datatypes. We argue that datatype-generic programming is sufficient to express essentially all the genericity found in the Standard Template Library. Moreover, datatype-generic programming is a precisely-defined notion with a rigorous mathematical foundation, in contrast to generic programming in general and the C++ template mechanism in particular, and thereby offers the prospect of better static checking and a greater ability to reason about generic programs. This paper describes work in progress.",
author = "Jeremy Gibbons",
booktitle = "Multiparadigm Programming",
editor = "J{\"o}rg Striegnitz and Kei Davis",
isbn = "3-00-016005-1",
note = "First International Workshop on Declarative Programming in the Context of Object-Oriented Languages (DPCOOL)",
pages = "277-289",
publisher = "John von {N}eumann Institute for Computing (NIC)",
title = "Patterns in Datatype-Generic Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/patterns.pdf",
volume = "27",
year = "2003",
}
@inproceedings{Gibbons2002:Superposition,
abstract = "Software architects such as Garlan and Katz promote the separation of \emph{computation} from \emph{coordination}. They encourage the study of \emph{connectors} as first-class entities, and \emph{superposition} of connectors onto components as a paradigm for component-oriented programming. We demonstrate that this is a good model for what \emph{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.",
author = "Jeremy Gibbons",
booktitle = "Coordination Models and Languages",
month = "apr",
pages = "166--173",
series = "Lecture Notes in Computer Science",
title = "Towards a Colimit-Based Semantics for Visual Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/superposition-extended.pdf",
volume = "2315",
year = "2002",
}
@book{Backhouse*2002:Algebraic,
abstract = "Program construction is about turning specifications of computer software into implementations. Doing so in a way that guarantees correctness is an undertaking requiring deep understanding of the languages and tools being used, as well as of the application domain. Recent research aimed at improving the process of program construction exploits insights from abstract algebraic tools such as lattice theory, fixpoint calculus, universal algebra, category theory and allegory theory. This book provides an introduction to these mathematical theories and how they are applied to practical problems.",
booktitle = "Algebraic and Coalgebraic Methods in the Mathematics of Program Construction",
editor = "Roland Backhouse and Roy Crole and Jeremy Gibbons",
issn = "0302-9743",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Algebraic and Coalgebraic Methods in the Mathematics of Program Construction",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/acmmpc-toc.pdf",
volume = "2297",
year = "2002",
}
@incollection{Bird*2002:Optimization,
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 a class of optimization problems, deriving efficient functional programs from concise relational specifications.",
author = "Richard Bird and Jeremy Gibbons and Shin Cheng Mu",
booktitle = "Algebraic and Coalgebraic Methods in the Mathematics of Program Construction",
editor = "Roland Backhouse and Roy Crole and Jeremy Gibbons",
issn = "0302-9743",
pages = "281--307",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Algebraic Methods for Optimization Problems",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/acmmpc-optimization.pdf",
volume = "2297",
year = "2002",
}
@incollection{Gibbons2002:Calculating,
abstract = "Functional programs are merely equations; they may be manipulated by straightforward equational reasoning. In particular, one can use this style of reasoning to \emph{calculate} programs, in the same way that one calculates numeric values in arithmetic. Many useful theorems for such reasoning derive from an \emph{algebraic} view of programs, built around datatypes and their operations. Traditional algebraic methods concentrate on initial algebras, constructors, and values; dual \emph{co-algebraic} methods concentrate on final co-algebras, destructors, and processes. Both methods are elegant and powerful; they deserve to be combined.",
author = "Jeremy Gibbons",
booktitle = "Algebraic and Coalgebraic Methods in the Mathematics of Program Construction",
editor = "Roland Backhouse and Roy Crole and Jeremy Gibbons",
issn = "0302-9743",
pages = "148--203",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Calculating Functional Programs",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/acmmpc-calcfp.pdf",
volume = "2297",
year = "2002",
}
@article{Hutton&Gibbons00:Generic,
abstract = "The approximation lemma was recently introduced as a simplification of the well-known take lemma, and is used to prove properties of programs that produce lists of values. We show how the approximation lemma, unlike the take lemma, can naturally be generalised from lists 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 by-product, we find that generalising the approximation lemma in this way also simplifies its proof.",
author = "Graham Hutton and Jeremy Gibbons",
journal = "Information Processing Letters",
month = "aug",
number = "4",
pages = "197--201",
title = "The Generic Approximation Lemma",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/approx.ps.gz",
volume = "79",
year = "2001",
}
@article{Martin&Gibbons2001:Semantics,
abstract = "Nested (or non-regular or non-uniform) 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 $\mathit{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 $\mathit{Nat}(\mathit{Set})$, with objects all endofunctors on $\mathit{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 \emph{cocontinuous} endofunctors and natural transformations. This category is then a suitable semantic domain for nested datatypes, both first order and higher-order.",
author = "Clare Martin and Jeremy Gibbons",
journal = "Information Processing Letters",
month = "dec",
number = "5",
pages = "233--238",
title = "On the Semantics of Nested Datatypes",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/semantics.ps.gz",
volume = "80",
year = "2001",
}
@article{Gibbons*2001:When,
abstract = "We give a necessary and sufficient condition for when a set-theoretic function can be written using the recursion operator fold, and a dual condition for the recursion operator unfold. The conditions are simple, practically useful, and generic in the underlying datatype.",
author = "Jeremy Gibbons and Graham Hutton and Thorsten Altenkirch",
journal = "Electronic Notes in Theoretical Computer Science",
month = "apr",
note = "Proceedings of Coalgebraic Methods in Computer Science",
number = "1",
title = "When is a Function a Fold or an Unfold?",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/kernels.ps.gz",
volume = "44",
year = "2001",
}
@article{Gibbons2000:Generic,
abstract = "A \emph{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 hoc way for just a couple of kinds of tree. We generalize the concept to an arbitrary regular datatype; the resulting definition is co-inductive.",
author = "Jeremy Gibbons",
journal = "Science of Computer Programming",
pages = "37--65",
title = "Generic Downwards Accumulations",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/genda.ps.gz",
volume = "37",
year = "2000",
}
@inproceedings{Bird*99:Program,
abstract = "It is well-known that each polymorphic function satisfies a certain equational law, called a \emph{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 \emph{higher-order} naturality property. One example is the operation \emph{unzip} that takes lists of pairs to pairs of lists. Surprisingly, this property can be invoked to improve the asymptotic efficiency of some divide-and-conquer 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.",
author = "Richard Bird and Jeremy Gibbons and Geraint Jones",
booktitle = "Millenial Perspectives in Computer Science",
editor = "J. W. Davies and A. W. Roscoe and J. C. P. Woodcock",
publisher = "Palgrave",
title = "Program Optimisation, Naturally",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/naturally.ps.gz",
year = "2000",
}
@inproceedings{deMoor&Gibbons00:Pointwise,
abstract = "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 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.",
author = "Oege de Moor and Jeremy Gibbons",
booktitle = "Algebraic Methodology and Software Technology",
month = "may",
pages = "371--390",
series = "Lecture Notes in Computer Science",
title = "Pointwise Relational Programming",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/pointwise.ps.gz",
volume = "1816",
year = "2000",
}
@unpublished{Gibbons99:Lecture,
annote = "Functional programs are merely equations; they may be calculated by straightforward equational reasoning. Many useful theorems for such reasoning derive from an \emph{algebraic} view of programs, built around datatypes and their operations. Traditional algebraic methods concentrate on initial algebras, constructors, and values; dual, co-algebraic, methods concentrate on final co-algebras, destructors, and processes. Both methods are elegant and powerful; they deserve to be combined.",
author = "Jeremy Gibbons",
month = "mar",
note = "Estonian Winter School on Computer Science",
title = "Lecture Notes on Algebraic and Coalgebraic Methods for Calculating Functional Programs",
year = "1999",
}
@article{Gibbons99:Pointless,
abstract = "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 help of an example, namely calculating the \emph{radix-sort} algorithm from a more obvious specification of sorting. The message that we hope to send is that point-free calculations are sometimes surprisingly simpler than the corresponding point-wise calculations.",
author = "Jeremy Gibbons",
journal = "Journal of Functional Programming",
number = "3",
pages = "339--346",
title = "A Pointless Derivation of Radixsort",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/radix.ps.gz",
volume = "9",
year = "1999",
}
@inproceedings{Gibbons&Hutton99:Proof,
abstract = "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 \emph{take lemma}, and coinduction. However, these methods are all rather low-level, 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 high-level algebraic properties of this operator to conduct proofs in a purely calculational style that avoids the use of either induction or coinduction.",
author = "Jeremy Gibbons and Graham Hutton",
booktitle = "Proceedings of 1st Scottish Workshop on Functional Programming",
title = "Proof Methods for Structured Corecursive Programs",
year = "1999",
}
@article{deMoor&Gibbons99:Bridging,
abstract = "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. \par We claim that the algorithm designer is forced to omit some of the details by the relative expressive poverty of the Pascal-like languages typically used to present the solution. The greater expressiveness provided by a functional language would allow the whole story to be told in a reasonable amount of space. In this paper we use a functional language to present the development of a sophisticated algorithm all the way to the final code. We hope to bridge the algorithm gap between abstract and concrete implementations, and thereby facilitate communication between the constructive programming and algorithm design communities.",
author = "Oege de Moor and Jeremy Gibbons",
journal = "Science of Computer Programming",
number = "1",
title = "Bridging the Algorithm Gap: A Linear-Time Functional Program for Paragraph Formatting",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/bridging.ps.gz",
volume = "35",
year = "1999",
}
@article{Gibbons98:Structured,
abstract = "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 higher-level styles such as object-oriented programming. We also argue that, once it has been decided to teach structured programming, Java is a reasonable language to choose for doing so.",
author = "Jeremy Gibbons",
journal = "SIGPLAN Notices",
month = "apr",
note = "Also in Fintan Culwin, editor, \emph{Proceedings of the Second Conference on Java in the Computing Curriculum}, South Bank University, London",
number = "4",
pages = "40--43",
title = "Structured Programming in Java",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/spjava.ps.gz",
volume = "33",
year = "1998",
}
@unpublished{Gibbons&Jones98:Against,
author = "Jeremy Gibbons and Geraint Jones",
note = "Oxford Brookes University and Oxford University Computing Laboratory",
title = "Against the Grain: Linear-Time Breadth-First Tree Algorithms",
year = "1998",
}
@inproceedings{Gibbons98:Polytypic,
abstract = "A \emph{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~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 \emph{path} in such a datatype.",
address = "Marstrand, Sweden",
author = "Jeremy Gibbons",
booktitle = "Proceedings of Mathematics of Program Construction",
editor = "Johan Jeuring",
month = "jun",
pages = "207-233",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Polytypic Downwards Accumulations",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/polyda.ps.gz",
volume = "1422",
year = "1998",
}
@inproceedings{Gibbons&Jones98:Underappreciated,
abstract = "\emph{Folds} are appreciated by functional programmers. Their dual, \emph{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 \emph{breadth-first traversal} of a tree. We specify breadth-first traversal in terms of \emph{level-order 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 breadth-first traversal directly as an unfold; this turns out to be the `standard' queue-based algorithm.",
address = "Baltimore, Maryland",
author = "Jeremy Gibbons and Geraint Jones",
booktitle = "International Conference on Functional Programming",
month = "sep",
pages = "273--279",
title = "The Under-Appreciated Unfold",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/unfold.ps.gz",
year = "1998",
}
@techreport{Gibbons97:Conditionals,
abstract = "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.",
author = "Jeremy Gibbons",
institution = "School of Computing and Mathematical Sciences, Oxford Brookes University",
month = "jan",
number = "CMS-TR-97-01",
title = "Conditionals in Distributive Categories",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/conditionals.ps.gz",
year = "1997",
}
@techreport{Gibbons97:More,
abstract = "In his paper \textit{On Merging and Selection} (\textit{Journal of Functional Programming} 7(3), 1997), Bird considers the problem of computing the $n$th 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.",
author = "Jeremy Gibbons",
institution = "School of Computing and Mathematical Sciences, Oxford Brookes University",
month = "oct",
number = "CMS-TR-97-08",
title = "More on Merging and Selection",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/merging.ps.gz",
year = "1997",
}
@inproceedings{Gibbons97:Calculating,
abstract = "A good way of developing a correct program is to \emph{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 \emph{maximum segment sum} problem). We show that calculations are driven by \emph{promotion}, and that promotion properties arise from \emph{universal properties} of the data types involved.",
author = "Jeremy Gibbons",
booktitle = "Proceedings of ISRG/SERG Research Colloquium",
editor = "Keiichi Nakata",
month = "nov",
note = "Technical Report CMS-TR-98-01",
organization = "School of Computing and Mathematical Sciences, Oxford Brookes University",
title = "Calculating Functional Programs",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/calculating.ps.gz",
year = "1997",
}
@inproceedings{Gibbons&Wansbrough96:Tracing,
abstract = "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 languages. In particular, it allows a one-dimensional textual representation of terms, rather than requiring a two-dimensional graphical representation using arrows. We describe a program LetTrace, implemented in Gofer and tracing lazy evaluation of a subset of Gofer.",
address = "Melbourne",
author = "Jeremy Gibbons and Keith Wansbrough",
booktitle = "Computing: The Australasian Theory Seminar",
editor = "Michael E. Houle and Peter Eades",
month = "jan",
pages = "11--20",
title = "Tracing Lazy Functional Languages",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/tracing.ps.gz",
year = "1996",
}
@article{Gibbons96:Computing,
abstract = "{\em 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 {\em 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 {\em logarithm\/} of the depth of the tree, on a CREW PRAM machine.",
author = "Jeremy Gibbons",
journal = "Theoretical Computer Science",
note = "Earlier version appeared in Proceedings of the 16th Australian Computer Science Conference, Brisbane, 1993",
number = "1",
pages = "67--80",
title = "Computing Downwards Accumulations on Trees Quickly",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/quickly.ps.gz",
volume = "169",
year = "1996",
}
@article{Gibbons96:Deriving,
abstract = "The {\em 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 specification, the starting point for the derivations, consists of a collection of intuitively appealing {\em 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. \par The algorithm consists of an {\em upwards accumulation\/} followed by a {\em downwards accumulation\/} on the tree, and is further evidence of the utility of these two higher-order tree operations.",
author = "Jeremy Gibbons",
journal = "Journal of Functional Programming",
number = "3",
pages = "535--562",
title = "Deriving Tidy Drawings of Trees",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/drawing.ps.gz",
volume = "6",
year = "1996",
}
@proceedings{Bridges*96:Combinatorics,
address = "Singapore",
editor = "Douglas Bridges and Cris Calude and Jeremy Gibbons and Steve Reeves and Ian Witten",
publisher = "Springer-Verlag",
title = "Combinatorics, Complexity and Logic: Proceedings of Discrete Mathematics and Theoretical Computer Science",
year = "1996",
}
@article{Gibbons96:Third,
abstract = "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 homomorphism - it can be computed according to any parenthesization of the list. We formalize and prove the theorem, and describe two practical applications: to fast parallel algorithms for language recognition problems and for downwards accumulations on trees.",
author = "Jeremy Gibbons",
journal = "Journal of Functional Programming",
note = "Earlier version appeared in C.\,B.\,Jay, editor, {\it Computing: The Australian Theory Seminar}, Sydney, December~1994, p.\,62--69",
number = "4",
pages = "657--665",
title = "The Third Homomorphism Theorem",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/thirdht.ps.gz",
volume = "6",
year = "1996",
}
@inproceedings{Gibbons95:Initial,
abstract = "The initial-algebra approach to modelling datatypes consists of giving {\em constructors\/} for building larger objects of that type from smaller ones, and {\em 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. \par We show how to model a particular kind of directed acyclic graph using this initial-algebra approach.",
author = "Jeremy Gibbons",
booktitle = "Mathematics of Program Construction",
editor = "Bernhard M{\"o}ller",
pages = "282--303",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "An Initial-Algebra Approach to Directed Acyclic Graphs",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/damgs.ps.gz",
volume = "947",
year = "1995",
}
@inproceedings{Gibbons95:Dotted,
abstract = "We show how to draw evenly dotted and dashed curved lines in Metafont, using {\em 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.",
author = "Jeremy Gibbons",
booktitle = "Proceedings of the 1995 Annual Meeting",
editor = "Robin Fairbairns",
organization = "\TeX{} Users' Group",
title = "Dotted and Dashed Lines in Metafont",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/dashed.ps.gz",
year = "1995",
}
@inproceedings{Gibbons94:How,
abstract = "The {\em 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 specification, the starting point for the derivations, consists of a collection of intuitively appealing {\em 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. \par The algorithm consists of an {\em upwards accumulation\/} followed by a {\em downwards accumulation\/} on the tree, and is further evidence of the utility of these two higher-order tree operations.",
address = "Department of Computer Science, University of Auckland",
annote = "Condensed version of \cite{Gibbons93:Deriving}",
author = "Jeremy Gibbons",
booktitle = "Proceedings of Salodays in Auckland",
editor = "C. Calude and M. J. J. Lennon and H. Maurer",
note = "Also in Proceedings of First New Zealand Formal Program Development Colloquium, p.\,105--126.",
pages = "53--73",
title = "How to Derive Tidy Drawings of Trees",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/nzfpdc-drawing.ps.gz",
year = "1994",
}
@article{Gibbons*94:Efficient,
abstract = "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. 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(\log n)$ time on $O(n/\log n)$ processors, which is optimal.",
author = "Jeremy Gibbons and Wentong Cai and David Skillicorn",
journal = "Science of Computer Programming",
pages = "1--18",
title = "Efficient Parallel Algorithms for Tree Accumulations",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/efficient.ps.gz",
volume = "23",
year = "1994",
}
@inproceedings{Gibbons94:Introduction,
abstract = "The Bird-Meertens 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 {\em data}, as opposed to {\em program}, structure. \par This paper presents a brief introduction to the philosophy and notation of the calculus, in the guise of the (well-known) derivation of a linear-time solution to the `maximum segment sum' problem.",
address = "Hamilton",
author = "Jeremy Gibbons",
booktitle = "Proceedings of the First New Zealand Formal Program Development Colloquium",
editor = "Steve Reeves",
month = "nov",
pages = "1--12",
title = "An Introduction to the Bird-Meertens Formalism",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/nzfpdc-squiggol.ps.gz",
year = "1994",
}
@inproceedings{Gibbons93:Upwards,
abstract = "An {\em accumulation\/} is a higher-order 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 function---in fact, some homomorphism---of that element's descendants and of its ancestors, respectively. These two operations can be thought of as passing information up and down the tree. \par We introduce these two accumulations, and show how together they solve the so-called prefix sums problem.",
author = "Jeremy Gibbons",
booktitle = "Mathematics of Program Construction",
editor = "R.~S. Bird and C.~C. Morgan and J.~C.~P. Woodcock",
note = "A revised version appears in the Proceedings of the Massey Functional Programming Workshop, 1992",
pages = "122--138",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
title = "Upwards and Downwards Accumulations on Trees",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/accumulations.ps.gz",
volume = "669",
year = "1993",
}
@inproceedings{Gibbons93:Formal,
abstract = "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 general, and in particular describes their successful role in specifying, constructing and proving correct the floating-point unit of the Inmos T800 transputer chip.",
author = "Jeremy Gibbons",
booktitle = "Proceedings of the 13th New Zealand Computer Society Conference",
editor = "John Hosking",
pages = "207--217",
title = "Formal Methods: Why Should I Care? The Development of the T800 Transputer Floating-Point Unit",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/formal.ps.gz",
year = "1993",
}
@techreport{Jones&Gibbons93:Linear,
abstract = "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 traversal algorithm, and of a subtle and efficient breadth-first tree labelling algorithm.",
author = "Geraint Jones and Jeremy Gibbons",
institution = "Dept of Computer Science, University of Auckland",
month = "may",
note = "Also IFIP Working Group 2.1 working paper 705~WIN-2",
number = "No.\,71",
title = "Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips",
url = "http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/linear.ps.gz",
year = "1993",
}
@inproceedings{Gibbons93:Computing,
abstract = "{\em 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 {\sc Crew Pram} machine.",
address = "Brisbane",
author = "Jeremy Gibbons",
booktitle = "16th Australian Computer Science Conference",
editor = "Gopal Gupta and George Mohay and Rodney Topor",
month = "feb",
note = "Revised version \cite{Gibbons96:Computing}",
pages = "685--691",
title = "Computing Downwards Accumulations on Trees Quickly",
year = "1993",
}
@phdthesis{Gibbons91:Algebras,
abstract = "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 Bird-Meertens formalism, a calculus for the construction of programs by equational reasoning from their specifications. \par We present three different tree algebras: two kinds of binary tree and a kind of general tree. One of the binary tree algebras, called `hip trees', is new. Instead of being built with a single ternary operator, hip trees are built with two binary operators which respectively add left and right children to trees which do not already have them; these operators enjoy a kind of associativity property. \par Each of these algebras brings with it with a class of `structure-respecting' functions called catamorphisms; the definition of a catamorphism and a number of its properties come for free from the definition of the algebra, because the algebra is chosen to be initial in a class of algebras induced by a (cocontinuous) functor. Each algebra also brings with it, but not for free, classes of `structure-preserving' functions called accumulations. An accumulation is a function that preserves the shape of a structured object such as a tree, but replaces each element of that object with some catamorphism applied to some of the other elements. The two classes of accumulation that we study are the `upwards' and `downwards' accumulations, which pass information from the leaves of a tree towards the root and from the root towards the leaves, respectively. \par Upwards and downwards accumulations turn out to be the key to the solution of many problems about trees. We derive accumulation-based algorithms for a number of problems; these include the parallel prefix algorithm for the prefix sums problem, algorithms for bracket matching and for drawing binary and general trees, and evaluators for decorating parse trees according to an attribute grammar.",
author = "Jeremy Gibbons",
note = "Available as Technical Monograph PRG-94. ISBN 0-902928-72-4",
school = "Programming Research Group, Oxford University",
title = "Algebras for Tree Algorithms",
year = "1991",
}
@article{Bird*89:KMP,
abstract = "This paper is devoted to the synthesis of a functional version of the Knuth-Morris-Pratt algorithm for pattern matching. This algorithm was first discussed by Knuth; since then formal developments have been given by Dijkstra and Dromey, among many others. The novel aspects of the present treatment are: (i) the result is expressed as a (very short) functional program; and (ii) the derivation makes use of the calculus of lists described by Bird.",
author = "Richard S. Bird and Jeremy Gibbons and Geraint Jones",
journal = "Science of Computer Programming",
month = "jul",
number = "2",
pages = "93--104",
title = "Formal Derivation of a Pattern Matching Algorithm",
url = "http://dx.doi.org/10.1016/0167-6423(89)90036-1",
volume = "12",
year = "1989",
}
@mastersthesis{Gibbons88:View,
abstract = "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 higher-order operators, encapsulating common patterns of computation on trees. We explore their use by deriving solutions to a couple of algorithmic problems on trees. \par The work proceeds in the Bird-Meertens style. This is a calculus for programs, closely related to applicative programming languages. Expressions are written at the function level, avoiding the use of unnecessary names and being as concise as possible. Derivations are performed by program transformation~--- the application of correctness-preserving transformations to an initial specification, with the intention of improving its efficiency without changing its meaning.",
author = "Jeremy Gibbons",
note = "Abstract appears in the Bulletin of the EATCS, number~39, p.~214.",
school = "Programming Research Group, Oxford University",
title = "A New View of Binary Trees",
year = "1988",
}
