Richard Banach received the degree of B.Sc. in Mathematical Physics in
1976 from Birmingham University (UK). This was followed in 1977 by a Diploma
in Advanced Studies in Science, and in 1979 by a Ph.D. in Theoretical
Physics, both from Manchester University (UK). The field of study for his
doctorate was quantum field theory in topologically non-trivial spacetimes.
There followed three further years as a researcher in theoretical physics,
studying quantum field theory.
In 1982 he joined International Computers Limited working on the development
of the ICL 3980 mainframe. There, his main areas of responsibility lay at
the hardware/software interface: from address translation microcode, through
the design and implementation of the global synchronisation primitives for
multinode systems, (the ICL 3900 series machines were probably the first
commercially available machines featuring a globally cache coherent,
physically distributed virtual memory model), and thence to multinode error
In 1986 he rejoined Manchester University, this time in the Computer Science
Department, as a lecturer. For the next few years he was associated with the
Alvey Flagship Project, a large multifaceted collaborative research enterprise,
whose objective was the design of a novel system architecture, encompassing
parallel hardware, a graph rewriting based computational model, applicative
programming models, novel operating system structures, and applications.
His work again included the hardware/software interface of the system, but
eventually concentrated on the design of the MONSTR language and
computational model, which became the definitive programmers' interface for
the Flagship machine. MONSTR is a term graph rewriting language which
constrains the flexibility of the unrestricted generalised term graph
rewriting model of computation, in such a way that direct execution on
parallel hardware becomes conceivable, without an excessive loss of
After Flagship berthed in the late 1980's, his interests become more
concerned with the theory of graph rewriting. MONSTR is a language which
is expressive enough to use in practice, but whose operational semantics
are simple enough to be amenable to rigorous study, and various questions
concerning the equivalence of different semantic models for the MONSTR syntax
occupied his attention; especially those which enable an implementation to
skimp on things like synchronisation and strict adherence to serialisability,
without destroying higher level conformance to a rewriting semantics.
The applicability of MONSTR for expressing in a natural manner various aspects
of novel programming paradigms as they gain popularity, is intermittently the
subject of publications. Further issues regarding the semantics of graph
rewriting have been of interest. These include the correspondence between the
term graph rewriting model and other graph rewriting models, such as the
double pushout approach; the categorical semantics of graph rewriting in
general, particularly fibration semantics (a particularly elegant abstract
diagrammatic semantics has been developed for the double pushout approach);
and the possibilities for type inference within graph rewriting formalisms.
One aspect of many of these topics that makes them particularly intriguing
is the absence of one of the theoretician's favourite tools, structural
induction, caused by the presence of cycles within graphs. Other research
interests have included: linear logic, particularly the correspondence
between proof nets, interaction nets, and conventional graph rewriting
formalisms; concurrency theory as expressed in the Pi-calculus, CCS,
and its comparison with graph rewriting; and the utility of regular relations
within specification disciplines.
Formal methods have become a major new area of activity, with some focus on
the B method, and especially as applied to problems described by continuous
mathematics, which plays such an important role in real world situations as
exemplified by embedded systems. This has obvious repercussions for safety-
critical system development. A recent advance has been the introduction of
the notion of retrenchment, which is a liberalisation of refinement,
permitting the controlled breaking of the proof obligations of refinement,
and permitting the mixing of I/O and state aspects of operations in the
passage from the abstract to the concrete model. Retrenchment generally
permits more of the informal aspects of engineers' model building to be
formally captured. Retrenchment resonates strongly with application builders,
who experience the limitations of the familiar refinement technique on a daily
basis. It also subsumes many previous attempts to break out of the
'refinement straitjacket' that are to be found in the literature.
Since 1996 Dr. Banach has been a senior lecturer.
He is a Foundation Editor of the Journal of Universal Computer Science.
Main Research Interests:
- Retrenchment, a means of formalising more of informal design. See the Retrenchment Homepage.
- Application of formal methods to problems involving continuous mathematics.
- Formal methods in general, particularly the B method.