Next: Swansea
Up: Cooperating sites
Previous: Sheffield


The logic groups of the departments of Mathematics in the universities of Stockholm and Uppsala have long experience in the fields of Type Theory, as well as in related fields like Category Theory, Topos Theory, Domain Theory, and Recursion Theory. Per Martin-Löf, the inventor of Constructive (or Intuitionistic) Type Theory, is the leader of the logic group in Stockholm. Constructive Type Theory is the major source of inspiration for most type theories under consideration in the TYPES network. The proof assistants ALF and AGDA, developed at the Chalmers University site, is based on Martin-Löf's type theory.

The group plans to contribute mainly to the Foundational Research project objective. This includes constructive and predicative development and formalization of mathematics; in particular Topology, Algebra, and Category Theory. The use of type-theoretical universes in such developments will be investigated.

The senior members of the logic groups are

Per Martin-Löf has given several invited talks in the TYPES workshops during the last couple of years. The group also had several visitors from other TYPES sites, e.g. Thierry Coquand, from the Chalmers site, and Nicola Gambino, from the Manchester site.

The group would like to cooperate in the near future with the Nijmegen site with the aim of mutually learning more about benefits and drawbacks of the different type theories in use.

Stockholm/Uppsala homepage

Bengt Nordström 2005-09-22