Research group Mathematical logic

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).

Seminars are announced in the calendar at Stockholm Mathematics Centre, SMC
Web pages including older seminars