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