Partial List of Publications
I'm in the process of reorganising my publications on the web: in the mean-time, here's a partial and not-very-up-to-date list.
The documents contained in these directories are included by the
contributing authors as a means to ensure timely dissemination of scholarly and
technical work on a non-commercial basis. Copyright and all rights therein are
maintained by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all
persons copying this information will adhere to the terms and constraints
invoked by each author's copyright. These works may not be reposted without the
explicit permission of the copyright holder.
My research interests are functional programming in general, and program
analysis and transformation in particular.
Some other exciting topics:
Specialisation for the Lambda-calculus; or, A New Paradigm for Partial
Evaluation based on Type Inference, presented at the Dagstuhl Seminar on
Partial Evaluation. Describes a partial evaluator which specialises not
only expressions, but types. So a universal type in an interpreter, for
example, may be specialised to arbitrary types in the residual versions.
This leads to optimal specialisation, that is, complete removal of a
layer of interpretation --- the first time this has been achieved for a
typed higher-order language. Other interesting results include the
combination of constructor specialisation with higher-order functions,
leading to `firstification for free'.
While previous partial evaluators have been, in a sense, generalised
evaluators, this one is a generalised type-checker --- hence the `new
- In addition to the full paper, there is a Glasgow
workshop paper that gives an informal introduction to the basic ideas.
- A paper on type
specialisation in imperative languages appeared in ICFP '97.
- A short
survey article appeared in Computing Surveys in 1998.
- A type
specialisation tutorial was presented at the DIKU Summer School on
Partial Evaluation. This article also describes a new type-based arity
raiser used as a post-processor, and shows new applications of type
specialisation to transforming polymorphic programs to monomorphic ones, and
modelling constructor specialisation by polyvariance. The examples in the
paper can be run on the online demo.
- I have proved
the correctness of the type specialiser.
- I spoke about type specialisation as a Strachey
Lecture in Oxford.
- There is a demo of
the partial evaluator available. You can if you wish get the sources.
There is also a new
version of the type specialiser available, which is nicer to use thanks
to some syntactic sugar, and which includes a type-based arity raiser.
- Per Sjörs has implemented a type specialiser for a subset of Haskell, as
his Masters project (Masters
I've also been working on `arrows', an alternative to monads for
structuring combinator libraries. I gave a talk on the subject at Mathematics
for Program Construction, and there is now a draft paper (pdf) available.
The final version appeared in Science of Computer Programming. Ross
Paterson maintains a web page on
arrows, including a nice proposal for adding syntactic sugar
In 2004 I presented a series of lectures on arrows at the
Advanced Functional Programming summer school in Tartu,
Estonia. Apart from presenting arrows in a tutorial manner, these
lectures included an arrow library for discrete event
simulation as an extended example.
Lars Pareto and I have combined our earlier work on sized types with
Tofte and Talpin's region types. The result is a type system for a small
strict functional language which can guarantee space bounds on the memory
needed to run the program -- even though the language has both recursion and
dynamic data structures. A paper appeared at
Here are some other papers. This list is not up-to-date, I fear: waiting for me to find a better way of organising my publications!
- Why Functional
Programming Matters, a tutorial paper on functional programming, whose
main thrust is that higher-order functions and lazy evaluation can and should
be used to make a substantial contribution to modularity in functional
programs. Dates from 1984, but I suspect is probably still my most widely read
A translation into
Russian is now available!
- Lazy Memo-functions, which shows how memo-functions can be provided in a lazy functional language, without making such functions hyper-strict. Also shows how such memo-functions can be used to improve program structure in a number of examples.
Analysis of Functional Programs, which suggests a framework for analyses
such as strictness analysis, escape analysis, and sharing analysis, and a way
of extending backwards analysis to higher-order functions. This paper appeared
at the workshop on Partial Evaluation and Mixed Computation in 1988.
Warning: This is a scanned version and it's BIG!
Loop-detecting Interpreter for Lazy, Higher-order Programs, a joint paper
with Alex Ferguson which appeared in the 1992 Glasgow Workshop on Functional
Programming. The interpreter described is based on Berry and Curien's theory
of sequential algorithms, and is able to detect a surprising variety of loops.
Abstract Interpretation Using Sequential Algorithms, another joint paper
with Alex Ferguson which appeared in the Workshop on Static Analysis, 1993.
This paper uses similar techniques to the previous one to find fixpoints
rapidly in the analysis of higher-order programs. (bibtex).
for strictness analysis, a joint paper with Phil Wadler,
which appeared in FPCA 1987. Describes a method for backwards strictness
analysis of first-order programs with complex data structures, whose
correctness is argued by modelling contexts as projections. (bibtex).
- Projections for
Polymorphic First-Order Strictness Analysis, a joint paper with John Launchbury which appeared
in J. Mathematical Structures in Computer Science in 1992. Applies categorical
properties of polymorphic functions to projection-based strictness analysis,
to show that analysing one instance yields results that apply to all. (bibtex).
Projection-based Strictness Analysis, a joint paper with Ryszard Kubiak
and John Launchbury which
appeared in the 1992 Glasgow Workshop on Functional Programming. Describes a
prototype implementation of the analysis for a subset of Haskell. (bibtex).
- Avoiding Unnecessary
Updates, a joint paper with John Launchbury, Andy Gill,
Simon Marlow, Simon Peyton Jones, and Philip Wadler, which appeared in the
1993 Glasgow Workshop on Functional Programming. Describes a type-based
analysis to discover when the updates needed to implement call-by-need are in
fact unnecessary. (bibtex).
Abstract Interpretations, a joint paper with John Launchbury which appeared
in ESOP in 1992. Shows how to `invert' abstract functions using Galois
connections, thus reversing the direction of an analysis. We reverse Burn,
Hankin and Abramsky's strictness analysis and thereby derive a more efficient
(although less accurate) backwards analysis from it. (bibtex).
- The Design of a
Pretty-printing Library, a chapter for the Spring School on
Functional Programming. The library defines five combinators for
constructing documents with alternative layouts, from which the `prettiest' is
then chosen. The combinators are specified formally and several alternative
implementations derived. The library is distributed along with the Haskell B.
compiler, and the source is also available here. (abstract, bibtex).
An Object-Oriented Extension of Haskell, a joint paper with Jan Sparud which was presented
at the Haskell Workshop in 1995. Haskell++ extends Haskell with `object
classes' and `object instances' which are analogous to the existing classes
and instances, but support inheritance. A simple
preprocessor translates into Haskell. Here is a ray-tracing
package in Haskell++, an undergraduate project. (bibtex).
Choices Lazily, a joint paper with Andrew Moran which appeared in
FPCA '95. It
concerns the semantics of McCarthy's bottom-avoiding choice in a language with
- Proving the
Correctness of Reactive Systems Using Sized Types, a joint paper with Lars Pareto and Amr Sabry, which
appeared in POPL
'96. Sized types can express concepts such as 'lists with at most 5
elements' and 'streams with at least 6 elements', and our type system can
check properties such as termination and liveness of programs in a simple lazy
functional language. (bibtex).
Datatypes in Haskell, which appeared in the 1999 Haskell workshop.
This paper proposes to improve Haskell's support for data abstraction, by
letting the programmer declare that datatypes such as sets are
well-formed only under certain conditions on their element types. These
conditions then need not be repeated when the set type is used, reducing the
changes that must be made if the set type is reimplemented with different
restrictions. The paper contains further applications and shows how to
implement Restricted Datatypes by a translation into the Hugs extension of
Analysis for Polymorphic Types (extended abstract), to appear in PSI 2001. This joint
paper with Rogardt Heldal
extends Dussart, Henglein and Mossin's work on polymorphic
binding-times to polymorphic types. Rogardt's thesis contains
much more detail.
- Global Variables in
Haskell, which discusses how to implement updateable global variables in
Haskell. Management overview: use implicit parameters. This is a draft; the
final version will appear as a pearl in JFP.
Monadic Programs with QuickCheck, Haskell workshop 2002.
Here is a reasonably up to date list of publications, and
here are some bibtex
Last modified: Thu May 31 08:26:16 MET DST 2001