Underlying the question of "good software" are the mathematical foundations of computing 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, see our Analysis And Verification theme. Mathematical foundations of computer science, and in particular of software, are a main research theme in SWS, which is also 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).
We study various behavioral equivalences and preorders for reactive systems, for instance to support the work in the theme on model learning & testing. As an example, in recent work we explored the use of action codes to define vertical implementation relations that link labeled transition system models at conceptually different levels of abstraction.
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.
Notably, the categorical notion of co-algebra forms an ideal abstraction technique, as it describes systems in terms of observations and provides a general notion of "state-based system", generalising widely occurring structures such as automata, transition systems and probabilistic systems. Of particular interest is the interaction with algebraic structure: this interaction occurs for instance in the semantics of programming language At SWS we work on the interaction algebraic and coalgebraic techniques, and their application to concrete analysis tasks of systems, such as automata learning.
The interaction between algebra and coalgebra is also apparent in concurrency theory. At SWS, for instance, we further develop algebraic models such as Kleene algebra and its extensions, together with coalgebraic decision procedures. We study notions of equivalence between (concurrent) systems through notions of behavioural equivalence and their intricate relationships with modal logics.
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.