|
This page gives brief outlines of some of the areas of interest of the
Algebra of Programming group. Cross-references to the
publication list
are given, and also some links to related web pages.
The following topics are included:
The main aim of the Algebra of Programming group is to
develop clear and concise notations for writing programs. Functional
programming, which might be thought of as `programming with
expressions' (as opposed to `programming with actions'), encourages
such clarity and concision. We are interested in expanding the
applications of functional programming to a wider range of problems,
and in better understanding how to exploit the particular features of
functional programming languages.
- Publications:
- Related links:
Functional programming is very elegant, but it turns out that
functions are somewhat restrictive, especially when trying to model
`specifications' as well as `implementations'. In particular, it is
often natural to want to under-specify a problem, if several possible
outputs are equally acceptable. Using a functional paradigm prohibits
such underspecification, requiring an implementation decision to be
made earlier than is desirable, and restricting available choice in
further development. Relations, on the other hand, easily model such
non-determinism; they also encompass other useful operations such as
converse and conjunction. This research aims to develop sound
foundations for relational languages, and to investigate programming
with relations.
- Publications:
- Related links:
One strength of modern functional programming languages is in
handling data-structures: automatic garbage collection and the absence
(or ubiquity) of references mean that data structure manipulation is
often much simpler and clearer than in traditional imperative
languages. However, some efficient data structures seem to require
impure languages features such as destructive updates; an ongoing
research problem is to explore and expand the boundaries of what can
be achieved efficiently in a purely functional paradigm.
A particular area of recent interest is that of nested
datatypes. In a so-called `regular' datatype
definitions, such as lists:
data List a = Nil | Cons a (List a)
recursive instances of the type have the same parameters as the defining
instance. In contrast, in a nested datatype such as power lists:
data Pow a = Zero a |
Succ (Pow (a,a))
the recursive instances can have different parameters. Such datatypes
seem capable of providing `structure invariants'; for example, power
lists have length exactly a power of two. We are trying to understand
the semantics and capabilities of such datatypes, and to see how they
influence programming.
- Publications:
- Related links:
This research aims to provide concise theorems capturing the use
of general algorithmic paradigms, such as dynamic programming and
branch-and-bound. Typical applications include algorithms for
sequence comparison, data compression and graph problems.
- Publications:
- Related links:
Hoare's Unified Theory of Programming gives a single framework for
describing the algebraic semantics of different programming
paradigms. This work aims to incorporate the missing parts of the
logic programming paradigm into this unified theory. This is achieved
via a shallow embedding of Prolog into a lazy functional
language, preserving both the declarative and the procedural reading
of the Prolog predicate. (In the standard approach to mapping logic
programs to functional ones, the declarative reading is lost.)
A related line of research is our work on compositional logic
programming. This aims to combine the benefits of logic programming
(very high-level declarative specifications, thanks to the absence of a
distinction between inputs and outputs) and functional programming
(compositionality, thanks to higher-order operators).
These goals are similar to those of the functional logic language and the
higher-order logic programming communities, but our methods are a little
different.
- Publications:
- Related links:
Ruby is a relational programming language suited to the design of
synchronous hardware. The derivation of a Ruby design from a
high-level specification proceeds by equational reasoning, in a
similar way to the derivation of an efficient functional program from
an obvious one. This research is to use such derivations to control
the complexity of large designs, and to improve the designer's
confidence in their correctness.
- Publications:
- Related links:
Generic programming is about raising the level of abstraction
of programs. Generic programs are polymorphic, but typically in a
wider sense than the traditional one. Thus, traditional polymorphic
programs might be parameterized by a type, working equally
well for (say) lists of integers, lists of characters, lists of
functions, and so on. A generic program might be parameterized by a
richer structure, such as a type constructor (eg lists vs trees),
another program (as in component-oriented programming), or even a
programming paradigm (eg functional vs relational
programming). Genericity has been recognized as an important concept
in both functional and object-oriented programming. A
theory of generic programming will clearly be very flexible and
powerful; the problem that we are trying to address is to control this
flexibility without overly restricting its use, yielding a
disciplined theory of meta-programming.
A three-year EPSRC-funded project on
Datatype-Generic Programming is concentrating on this
topic.
- Publications:
- Related links:
An inductive program has a structure that reflects the structure of
its inputs; for example, the function sum, which sums a list
of integers:
| sum [] |
= |
0 |
| sum (x:xs) |
= |
x + sum xs |
Dually, a coinductive program has a structure that reflects
the structure of its outputs; for example, the function
range, which generates a list of integers:
| range (m,n) |
= |
[], |
if m>n |
|
= |
m : range (m+1,n), |
otherwise |
Note that with sum, the list constructors appear on the
left-hand side, whereas with range they appear on the
right.
Inductive programming has been well explored, and is well understood,
but it is only half of the story. We are investigating coinductive
programming, the other half; we hope to make it as popular and as
widely accepted.
- Publications:
- Related links:
Jeremy Gibbons
(Jeremy.Gibbons@comlab.ox.ac.uk)
|
![[Oxford Spires]](/im/spires.gif){kind=small}
oucl