Relational Methods in Computer Science
Relations are everywhere.
Element-free formalizations based on relations are often easier to handle
and more concise then traditional formalizations based on
elements and (partial) functions.
Proofs about relational formalizations tend to be calculational
and are therefore easier to check than the usual prose-based
predicate-logic-like proofs about traditional formalizations.
In short:
Relation algebra is a useful tool for concise and precise formal reasoning.
My interest in relation algebra originally mainly comes from the user perspective:
- My research on second-order term graphs
[Kahl-1996, Kahl-1995a, Kahl-1998a]
and other advanced variants of term graphs [Kahl-1998d] uses relational formalizations to cope with the consideral complexity of these topics.
- For these purposes I developed a very general kind of
Graphical Calculi of Relations,
designed for intuitive but formal reasoning with
or Relational Diagrams [Kahl-1996a, Kahl-1999d].
I am also interested in more general and foundational aspects:
- I am leading development of the
RATH framework
for relation-algebraic programming in Haskell.
- I am also working on
mechanised support for calculational reasoning
as usual in relational algebras
by producing a set of
Isabelle/Isar
theories covering different kinds of allegories and Kleene algebras,
including Dedekind categories and relation algebras,
see [Kahl-2003c].
- In
``A Relation-Algebraic Approach to Graph Structure Transformation''
I used relation-algebraic abstractions
to merge existing approaches to graph transformation
into a new approach that includes a natural graph variable concept.
- For better structuring of relational system specifications,
I introduced a
parallel composition
operator into the demonic calculus of relations.
- For the multi-authour book ``Relational Methods in Computer Science'' I acted as a co-editor.
- An investigation on the powerful relation algebraic tool of
symmetric quotients is
[Furusawa-Kahl-1998].
Furthermore I am involved in the international
community as:
- Organizer of the ETAPS 2001 Satellite Event RelMiS,
Relational Methods in Software
RelMiS,
- Maintainer of the home page,
- Administrator of the mailing list.
Wolfram Kahl