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