Underlying the question of "good software" are the formal structures that we use to model computation and software. We are concerned with the question of the meaning of a program or programming language, and how to best model this mathematically. Here the "best model" is related to the question of how intuitive the mathematical concepts are and whether they give rise to techniques that can be implemented in computer tools. The research in this theme belongs to the general area of formal methods. Our research on formal structures is also quite visible in the MFoCS (Mathematical Foundations of Computer Science) master track that we are responsible for.
Below, we outline our expertise in a number of focus areas.
Type theory is both a foundation of programming, especially functional programming, and a foundation of mathematics (as a competitor of set theory). It enables the study of programming concepts , in isolation or combined with other concepts, in an abstract mathematical setting, abstracting away from implementation details. But it also allows to make (part of) these implementation details explicit in case they are relevant for the program. Very powerful type theories include dependent types, higher order types, inductive types and homotopy types, and they allow the formalization of mathematics and mathematical proof. Thus they are ideally suited to form the basis of a "Proof Assistant" that integrates programming and proving in one computer tool. In SWS we use and contribute to Coq, but we also use other proof assistants based on type theory for the formalization of programming and mathematics and for verifying software.
In the context of specifying and verifying programs, it is desirable to study logics that are different from classical logic. One can add modalities to reason about recursion or time, or one can restrict logic to be substructural (affine or linear) so that it becomes suitable for reasoning about resources (e.g., pointers) or concurrency. In SWS we develop such logics, study their semantics (e.g., Kripke models), their correspondence to type systems (via logical relation models and the Curry-Howard correspondence), and apply them to program verification (e.g., concurrent separation logic).
The fundamental question of the "meaning" of a program is studied by the field of semantics: it gives a mathematics description of the meaning of a program, either in an "operational style" (how does the program compute?) or in a "denotational style" (what mathematical function does the program describe?). This semantics is crucial in understanding programs, and computer artefacts in general, as it allows to abstract away from implementation details and to detect the general patterns. Category theory offers a rich mathematical "language" for defining semantics.
Term rewriting provides a simple but very powerful mathematical model of computation, where many notions that appear in programming can be studied in isolation. It forms the basis of functional programming and enables the study of concepts like the complexity of programs, evaluation strategies and higher order programs.
We study a group of formal languages that is often used in both automatic and human-guided theorem provers, and forms the theoretical foundation of functional programming languages. We develop methods to verify properties of such systems, and tools to apply these methods fully automatically. In particular, we consider the study of termination (given an algorithm specified as a higher-order term rewriting system, and given any input, will it eventually produce an output?), complexity (how quickly will it produce such an output?), and equivalence (will it produce the same output as another system executed on the same input?).