### Uppsala University

I. Moerdijk (Utrecht) and E. Palmgren are continuing their
investigations of predicative aspects of topos theory and the relation to
Martin-Löf type theories. Palmgren visited Utrecht in November 1998
and for a week in July 1999 (though not on TYPES WG grants). Palmgren
attended the TYPES meeting in Lökeberg, Sweden.
Anton Setzer has together with Peter Hancock during a visit at
Edinburgh developed a formulation of interactive programs in type
theory. This extends the IO monad to dependent types, adds additional
features like rebinding and while loops and allows general input
output commands as a parameter. He has worked on philosophical
foundations of type theory, analyzed meaning explanations for
universes in type theory and showed why a universe containing itself
cannot be justified. He has participated at the TYPES meeting in
Lökeberg, Sweden, where he talked about this topic. During visits of
M. Rathjen in Leeds, England, of G. Jäger and T. Strahm in Bern,
Switzerland and of T. Arai in Hiroshima, Japan he has -- apart from
pure proof theoretic investigations -- worked on proof theoretical
strong extensions of type theory, where he conjectures to have reached
Pi_n-reflection, Pi_alpha-reflection and finally the strength
of one stable ordinal with one admissible ordinal above it, which
would be the strongest constructive extension of type theory, coming
very close to the strength of Pi^1_2-comprehension axiom. He is
working on making use of these extensions as powerful data types.

#### Publications 1999, as relevant for TYPES:

A. Setzer, P. Dybjer: A finite axiomatization of
inductive-recursive definitions. 14 pp., 1998. In: Proceedings of TLCA 1999,
LNCS 1581, pp. 129 -- 146.

P. Dybjer and A. Setzer: Finite axiomatizations
of inductive-recursive definitions. Electronic Proceedings of the
workshop on generic programming, Marstrand, Sweden.
http://wsinwp01.win.tue.nl:1234/WGPProceedings/Preface.html

P. Hancock and A. Setzer: The IO monad in dependent
type theory. Electronic Proceedings of the Workshop on Dependent Types
in Programming,
http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/dtp99.html.

I. Moerdijk and E. Palmgren. Wellfounded Trees in
Cageories. (submitted)

I. Moerdijk and E. Palmgren. Predicative type theories, toposes
and CZF. (in preparation)

** Next:** University of Torino
** Up:** Progress Report
** Previous:** Queen Mary and Westfield College,
University of London