Research
Research in logic at the mathematics department was initiated in the late 1960s with Per Martin-Löf and his seminal work on proof theory and type theory, and its applications to the foundations of constructive mathematics. Martin-Löf type theory is a widely used foundational theory both in computer science for checking and organizing formal proofs, and in logic as a touchstone for constructiveness. Much of the present research efforts in the group may be regarded as a continuation of this internationally influential research program. New connections with topology and category theory, especially homotopy theory, has arisen with the univalent foundations program.
Some specific research topics:
- Systems for the foundations of constructive mathematics: Type theory, especially Martin-Löf type theory and univalent foundations, constructive set theory, computer supported formalization (Agda, Coq)
- Category theory and Model theory of constructive systems: categorical logic and model theory, homotopy-theoretic models of type theory, internal models of type theory.
- Constructive mathematics: point-free methods in topology and analysis. Logic and Linguistics: constructive and computational semantics.
Seminars
- The Stockholm Logic Seminar meets regularly on Wednesdays 11.00 – 11:45. Organizers: Peter LeFanu Lumsdaine, Anders Mörtberg, Per Martin-Löf (emeritus).
- Web pages including older seminars: http://logic.math.su.se/seminar/
