Featured Image (Width 750px, Height 340px)
Featured Image Caption
Featured Image Credit
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