Richard Banach: Mini CV

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
recovery strategy.  

In 1986 he rejoined Manchester University, this time in the Computer Science
Department, as a lecturer, and since 1986 a senior 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 expressivity.  

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 been a major area of activity for some time, with a 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.  One 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.

Most recently, the increasing popularity of real-world systems that contain
components that interact with the physical world, so-called cyberphysical
systems, has led to a redirection of the existing formal methods interests
towards methodologies for the top-down design and development of such systems.
In particular, it has led to the development of Hybrid Event-B, an extension
of the B-Method for top-down design and development of cyberphysical systems.

Dr. Banach regularly acts as a reviewer for work in the formal methods area,
and is a Foundation Editor of the Journal of Universal Computer Science.