Bigraphical Programming Languages: Starting with the Bigraphical Programming Languages project joint with Robin Milner, there have been a series of research projects affilliated to the PLS group researching the design of
a framework for construction and analysis of domain-specific models and programming languages based on the theory of bigraphs. The efforts have resulted in several PhD thesis extending the [1 theory of bigraphs and tools for editing and exploring bigraphical models].
Possible Ph.D. topics include investigations into applications of bigraphs to cyper-physical computing, business process modelling, systems biology and model-driven software engineering; development of tool support for (semi-)automatic verification of properties of bigraphical models; and extensions to the theory of bigraphs, e.g. type systems and quantitative analysis.
Contact: [2 Thomas Hildebrandt]. Modular Reasoning about Software: The goal of our research on modular reasoning about software is to develop theories and methods for modular reasoning about software written in modern programming languages. The purpose is to lay the foundation for improvement of software tools, which are being and will be developed over the next five to ten years and which will be used to improve software practice.
Possible Ph.D. topics include modular reasoning about shared heap objects (e.g., using variants of higher-order separation logic), parametricity for low-level code, and modular reasoning about higher-order store. Tools and Methods for Scalable Software Verification: The goal of this research project is to develop tools for practical verification of modern object-oriented software written in Java / C#. The project will be based on earlier developments in separation logic to reason about shared heap objects and on static analysis techniques, in particular abstract interpretation.
Possible Ph.D. topics include developments of separation logic for reasoning about delegates, generics and inheritance; specification and verification of the C5 collection library; development and implementation of tools based on abstract interpretation.
Logical Frameworks: The logical framework group is concerned with the development and implementation of meta-languages for advanced data structures as well as tools for programming with and reasoning about them. Those data structures include not only lists and trees (including abstract syntax trees) but also more complex data structures for the meaning of programs and the meaning of mathematical proofs. The main activities of the group focus on the development of the Twelf proof assistant, the functional programming language Delphin, digital libraries for mathematical knowledge, meta logics for LF and LLF, proofs by logical relations, logic programming, proof planning by proof abstraction, and complexity analysis of logic programs. A small but by no means complete list of ideas for doctoral theses include the meta theory of concurrent systems (such as CLF), meta reasoning by coinduction, disproving false conjectures, and complexity analysis of CLF programs. Concurrency Theory and Applications: There is an active group of researchers focusing on concurrency theory and applications within the PLS, focusing on behavioural (session) types, operational and denotational semantics of concurrent processes and applications within security, web-services, business processes and workflow.
The research is founded in the theory of process calculi, types, categorical models for concurrency and verification.
Contact: [3 Thomas Hildebrandt] and [4 Marco Carbone]. Models for guarded recursion: This project investigates type theories with delay operators and guarded recursive types and terms, with the aim of providing the foundation for extensions of proof assistants such as Coq and Agda. These extensions should be useful in two ways: as a new type system for programming with infinite structures, using the delay operators to provide a guarantee of termination expressible in types, and to allow for models of advanced programming languages to be constructed using solutions to guarded recursive type equations.
We study these type theories primarily using models constructed in category theory.
This is a theoretical project in the intersection between programming language theory and foundations of mathematics.
Contact: [5 Rasmus Møgelberg]