The group develops new models and logics for programming languages and type theories, using a variety of semantic techniques, ranging from operational semantics to category theory.

Currently, our focus is on developing new models and logics for modular reasoning about concurrent, higher-order, imperative programs; on models for type theories with guarded recursion, and on language-based security.

We have developed some tutorial material: the MoDuRes in Coq Tutorial and A Taste of Categorical Logic - Tutorial Notes, which was used as teaching material for the Oregon Programming Language Summer School 2014 aimed at other PhD students in the field.

The research group started in 2013 when Professor Lars Birkedal came to Aarhus University from the IT University of Copenhagen. Since then, several faculty members have joined the group, which today is a mix of faculty members, PhD students and postdocs from other leading groups around the world.

The group specializes in the development of new models and logics for reasoning about programs and develops new theory and prototype implementations.