The Programming, Logic and Semantics Group (PLS)

The Programming, Logic and Semantics group conducts basic research in programming languages and logic. The group coordinator is Rasmus Ejlers Møgelberg.

The researchers of the PLS group develop new logics for expressing and proving properties of programs. These logics can be used to e.g. prove that a program meets a specification, or that certain kinds of undesirable program behaviour will not occur. The latter could for example be deadlocks, which happens when a group of communicating processes all stall, waiting for messages from each other. The group also develops new programming languages and type systems for programming languages. The purpose of this type systems is often to ensure that all programs satisfy a particular property, e.g. that they do not leak data. 

The research projects in the group span from the development of tools for verification of Java-programs to the design of new programming languages. Some projects are primarily theoretical in nature, others are concerned with the application of logics and implementation of tools. 

See the research of the PLS Group