Logic and Types

Dependent Type Theory

The work on dependent type theory involves both theoretical investigations of syntax and semantics, and implementation and applications of proof assistants. A major topic of interest is homotopy type theory, including cubical type theory, synthetic homotopy theory, and synthetic algebraic geometry.

Implementation of Proof Assistants

The group is world renowned for its work on the design and implementation of proof assistants.

Since the 1990s the group has developed the proof assistant and dependently typed functional programming language Agda. Agda is an interactive system for writing and checking proofs and is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has inductive families, parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program.

Homotopy Type Theory

Our group designs type theories tailored for use in specific mathematical settings, lays the semantic groundwork to justify these theories, and applies them in practice. A particular focus is homotopy type theory (HoTT), which connects the notion of equality in type theory to higher homotopical structure and serves as a language for constructive homotopy theory. We also study higher category theory and abstract homotopy theory, in particular to understand models of HoTT and in the context of constructive mathematics.

Synthetic Algebraic Geometry

In algebraic geometry, polynomial equations are studied using methods from geometry and algebra. These two fields have many links, the most basic being the correspondence between a space and the algebra of functions from that space to a fixed ring. In the usual analytic approach, this correspondence is made one-to-one by using a complicated notion of space. In our synthetic approach, this correspondence is assumed one-to-one as an axiom. We were able to reproduce many non-trivial algebraic geometry results with this synthetic approach.

For more information on the project and references, visit the project website.

Graph Theory

The unit’s research in the field of algorithmic graph theory has its focus on NP-hard graph-theoretic problems. The main interest is to determine which graph properties allow for efficient algorithms and explore the limits of tractability. Part of the work uses the framework of parameterized complexity to obtain a more refined understanding of problems’ complexity.

Quantum Computing

The unit’s research into quantum computing is part of the project QuantumStack in collaboration with WACQT (Wallenberg Center for Quantum Technology).

We are applying the techniques of type theory and category theory to construct new languages representing the intermediate stages of translation when compiling an algorithm for a quantum computer from a quantum circuit designed by the user, into the sequence of microwave pulses that are sent to the quantum chip. The aim is to produce a compiler for a quantum computer that provides a formal guarantee of correctness.

Teaching

The unit's members teach a diverse range of courses at both the bachelor's and master's levels. These include fundamental topics such as Python programming, data structures, databases, web applications and automata theory, as well as more advanced subjects like mathematical modeling, computation models, programming language technology, advanced functional programming, logic in computer science, and a course in type theory where students learn to use the Agda system to verify program properties.

Moreover, members of the unit supervise numerous bachelor’s and master’s theses projects each year. Students interested in pursuing a thesis in any of the unit's areas of expertise are encouraged to reach out to its members.

The unit has also supervised graduate reading courses on several occasions, covering topics such as category theory, higher-order categories, and homotopy type theory.

Members of the Unit