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.
You can also read more about Professor Lars Birkedal here.
The research group started in 2013 when Professor Lars Birkedal came to Aarhus University from the IT University of Copenhagen.
Since then three new PhD students and four postdocs have joined, and, in August 2014 Aslan Askarov came from Harvard to start as Associate Professor.
The group is a mix of students and postdocs from other leading groups around the world, both international and Danish.
The group specializes in the development of new models and logics for reasoning about programs and develops new theory and prototype implementations.