Our group tackles the following **research themes**:

- Concurrency theory
- Equational reasoning
- Multi-agent systems
- Programming methodology
- Decision support systems

## Concurrency Theory (headed by Dr. Jorge A. Pérez)

We study the formal specification and analysis of concurrent systems. Our focus is on models of communicating programs and their associated validation techniques.

Concerning specification, our research focuses on **process calculi**, formal languages that express the interaction of concurrent processes in a compositional style. Concerning analysis, we study type systems for process calculi, often referred to as **behavioral type systems**. Intuitively, types represent the structured protocols that a channels/endpoints in a process specification should implement.

By coupling process calculi with behavioral types, we obtain a compositional approach to the validation of safety and liveness properties on specifications of communicating systems.

A particular class of behavioral types is session types, and thus one talks of **session-based concurrency** to refer to concurrent processes which adhere to protocols specified as session types.

Another class of (behavioral) type systems is the one induced by the **Curry-Howard correspondence for concurrency** ("propositions as sessions"), which connects message-passing concurrency and Girard's linear logic in the style of the well-known Curry-Howard correspondence ("propositions as types").

## Equational Reasoning (headed by Prof. Dr. Gerard R. Renardel de Lavalette)

Equational reasoning is a well-known kind of mathematical reasoning that is practised e.g. in algebra and in many correctness proofs. Its standard formalisation is equational logic, a simple but very general reasoning system that is often used in computing science, e.g. in algebraic specification and rewrite systems (Mathematica is a well-known example). Proof theory for this logic, addressing structural properties of equational proofs, hardly exists, and we try to fill in the gap.

## Multi-agent Systems (headed by Prof. Dr. Gerard R. Renardel de Lavalette)

Multi-agent systems (MAS, also known as Agent Computing or just Agency) is a subdiscipline of both Computing Science and Artificial Intelligence. Agents are intelligent, possibly mobile processes to which intentions can be attributed: beliefs, desires and commitments. A multi-agent system consists of agents that cooperate to perform a task. As an example, think of a travel agency trying to compose a holiday trip that best fits the client's wishes: this requires collaboration between the agents that perform subtasks such as hotel booking and airplane reservation. MAS is inspired by process theory and concurrency on the one hand, and logic and formal specification on the other hand. Process theory and concurrency provide the notion of concurrent and communicating processes; logic and formal specification provide high-level languages for description of and reasoning about agents and their intentions.

Some years ago, the group started to study some topics on the logical side of MAS: dynamic logic, epistemic logic, knowledge game theory. Recently, the group decided to investigate MAS also from the perspective of (concurrent) programming.

## Decision Support Systems (headed by Prof. Dr. Gerard R. Renardel de Lavalette)

The research in decision support systems focuses on medical real-time support systems (e.g. monitoring and warning systems for anesthesia and intensive care). For a smooth interaction with the user, such systems must have some kind of user awareness, i.e. they must know about the cognitive activities and the mental state of the user. This research subject combines two disciplines: human-computer interaction and artificial intelligence.

## Programming Methodology (headed by Prof. Dr. Wim H. Hesselink)

For programming methodology, the group aims to contribute to the design, specification, and verification of sequential, parallel and distributed algorithms, programs, and systems, possibly with assistance of a mechanical theorem prover.