The results for (1) are the following. Drs. M. Stefanova has completed and defended her thesis, entitled `Properties of Typing Systems' (22/6/99). Barendregt and Dekkers (together with co-authors) have worked on a seminal book on typed lambda calculus, of which volume 1 should be finished in 2000. Geuvers has worked on extending type theory with user-programmable proof search methods, via the addition of a fixed point combinator, see [1].
The results for (2) are the following. Drs. M. Ruys has completed his thesis, entitled `Studies in Mechanical Verification of Mathematical Proofs' (29/6/99). Geuvers and Wiedijk have worked on the formalization of constructive analysis in Coq, working towards the Fundamental Theorem of Algebra. This work was done in cooperation with Dr. R. Pollack from Edinburgh. In the Types99 workshop in Lokeberg, Sweden, the first part of this work was presented. Capretta has worked on formalizing Universal Algebra in Coq and presented this work in the workshop `Theorem Proving for Higher Order Logic' [2].
[1] Herman Geuvers, Erik Poll and Jan Zwanenburg, Safe Proof Checking in Type Theory with Y, in Proceedings of Computer Science Logic 99.
[2] Venanzio Capretta, Universal Algebra in Type Theory, in Proceedings of TPHOLs'99.