I am working in a branch of computer science called Formal Methods, which has the practical objective of making systems (primarily computerized, but not only) more reliable, and the foundational objective of gaining a better understanding of how reasoning processes work and can be implemented on a machine, and how knowledge is structured and can be represented and transformed.
In my PhD thesis, I have explored reasoning principles in a type theory that combines an expressive logic with functional programming constructs, and have collaborated in the development of a proof assistant implementing this theory. After a short escape as quality assurance engineer in the automotive industry, I have returned to academia, joining a larger project on compiler verification. The idea here is to precisely capture the semantics of programming languages and to show that the semantics is preserved by a translation process.
Triggered by an industrial collaboration, I have started applying formal, computer-supported reasoning in the area of model-driven development, which is at first glance primarily an engineering discipline. By abstracting from this particular domain, it becomes clear that the underlying graph structures are of more general interest, not only in computer science (pointer structures, communication networks) but also in natural sciences like biology and chemistry. With the growing popularity of graph databases, I become increasingly interested in using graph structures in knowledge representation systems with powerful inference capabilities. In a technical sense, questions of decidability and computable feasibility of these formalisms are of great relevance. On the practical side, a major future challenge is to make the technical apparatus accessible to non-experts, to explore applications in the natural sciences or humanities, and to obtain consistent symbolic knowledge from badly structured, often sub-symbolic data, a question that is at the core of current research in Artificial Intelligence.