Theoretical Computer Science
The people of this section are interested in:
- Lambda calculus and rewriting
- Process algebra
- Semantics of programming languages
- Type theory and proof checking
Our group has a rich research tradition in term rewriting and lambda calculus. The field encompasses the vast area of first- and higher-order term rewriting, lambda calculus (typed and untyped), and includes related areas such as graph rewriting. We mention the fundamental concept of orthogonality, which has always been a binding notion in our approach to rewriting and continues to be so. In recent years our research has focused on infinitary rewriting, termination techniques for first- and higher order rewriting, the application of rewriting to functional programming and the use and development of automated tools. Presently, we are exploring new applications of 'classical' term rewriting and lambda calculi, in the direction of mathematics, notably the study of braids and the braids monoid, the connection of infinitary rewriting for hypercomputation (including infinite time Turing machines), and the emerging family of lambda calculi connected with quantum computing.
Also new promising applications in the foundations of functional programming are investigated, to wit a (by now established) contribution of lambda calculus with patterns, and efforts to integrate the tools we have developed for recognizing and deciding stream productivity. Our specification schemes for infinite objects are also of importance for inclusion in proof assistants such as Coq, which have, as is well-known, only a limited facility for specifications of infinite recursive objects such as streams.
Process algebra is an algebraic language for describing system behavior. Fundamental to process algebra is a parallel operator, to break down systems into their concurrent components. A set of equations is imposed to derive whether two terms are behaviourally equivalent. We study fundamental questions regarding the equational theories underlying process algebras. Typical research challenges are the geometric aspects of process graphs, and (in)axiomatizability of particular process algebras. Also we investigate structural operational semantics that formally links a process algebra term to its process graph. Research challenges here are congruence properties, conservative extension, and decomposition of modal logic formulas. Methods from algebra and logics are employed for the unambiguous description of distributed systems. A wide range of analysis techniques and dedicated tools are used to prove that programmed systems exhibit their expected functionality. An important vehicle for us is the language mCRL for system verification, based on process algebra in combination with abstract data types.
Coalgebra, which is a dual of the classical algebraic approach, can be used for the modelling of and reasoning about various kinds of dynamical systems, both mathematical and software. It emphasizes a `black box' view on systems, and models their behaviour in terms of well-defined and restricted interaction through both observations and operations. It is being applied to the semantics, specification, and proof theory of programming languages, and to the modelling of coordination of component based software systems.
The general theme of the research in our group is algebraic techniques for the specification and analysis of systems. We aim to perform high-quality research on term rewriting, lambda calculus, process algebra, operational semantics, and coalgebra. More information can be found under research projects.
