Logic and Types

Our research is in the general area of logics and semantics of programs. Much of our work concerns intuitionistic type theory and its applications to program correctness and the formalization of mathematics. Our department has been in the forefront of this development since 1980. Among other things we have implemented several well-known proof assistants for intuitionistic type theory, including the Agda system.

Currently, we are working in the following areas:
  • Intuitionistic type theory
  • Homotopy​ type theory and univalent foundations
  • Proof assistants (Agda)
  • Certified programs and proofs
  • Fixed point logics
  • Type systems for privacy
  • Constructive mathematics

Published: Tue 24 Apr 2018. Modified: Fri 02 Nov 2018