The Life of the Lüth

Personal

Born 1966 and subsequently raised in sunny Lübeck at the shores of the Baltic Sea in north Germany. I left in 1986 for Berlin to study Computer Science at the Technische Universität Berlin. Moved again in 1991, this time to even sunnier Edinburgh, Scotland's beautiful capital, where I did a PhD at the Laboratory for Foundations of Computer Science at the University of Edinburgh. Came to the Universität Bremen in 1996, first as a research assistant, then as a Wissenschaftlicher Assistent.

After I finished my habilitation in 2005, I joined the research group for safe and secure cognitive systems of the newly-founded Bremen Lab of the German Research Centre for Artificial Intelligence (DFKI) as a senior researcher and vice head (research manager) of the group. My research is concerned with safe and secure systems, in particular safe robotics.

Research

My research covers the whole area of formal software development, from theoretical foundations as found in the theory of enriched monads to tool development and applications in practical areas such as robotics.

In my thesis, I have developed a compositional semantics for term rewriting systems which is based on the theory of enriched monads. This grew into a wider initiative to use methods from category theory in term rewriting, spear-headed by Neil Ghani and his group from the University of Leicester (now Nottingham). Recently, we have developed a method to prove abstract modularity results.

After arriving in Bremen, together with other colleagues we developed various tools to support formal program development, such as the transformation system TAS, the Casl Consistency Checker, and various extensions for the tactical theorem prover Isabelle, including a graphical user interface. My habilitation gives a good overview of my research in the last five years.

Since I joined the DFKI at the start of 2006, my research in formal program development is focussing on three areas:

Reuse and abstraction: I am the principal researcher in the AWE project, where we investigate the generalisation and abstraction of formal program developments.
User interfaces for theorem provers and related tools. Together with David Aspinall, we are developing the Proof General Kit; part of this project is supported by IBM. (See also the UITP'03 and UITP'05 workshops).
Formal methods for robotics, as in the SAMS project (which is just about to start).