Next: University of Oxford Up: Progress Report Previous: University of Helsinki

University of Manchester

Aczel continued working on the problem of determining the logical strength of the impredicative type theories of Lego and Coq. This has led to an investigation of the Russell-Prawitz modality, see [3], and was also the focus of [5]. Aczel took part in the Types'99 workshop and also in the IMLA workshop in Trento in July 1999 where he gave a talk on the Russell-Prawitz modality. He also made a short visit to Padua.

The final version of Anthony Bailey's thesis [4] was submitted in March and is in the process of being approved.

Nicola Gambino visited Manchester, from Padua, for the academic year as an Erasmus student and wrote his lauria thesis, see [5], under the joint supervision of Silvio Valentini (Padua) and Aczel.


[1] Aczel, P. Notes on the Simply Typed Lambda Calculus in Computational Logic, edited by U. Berger and H. Schwichtenberg, the Proceedings of the 1997 Advanced Study Institute International Summer School at Marktoberdorf, Springer-Verlag sub-series F: Computer and Systems Sciences of the NATO Advanced Science Institutes Series. ISBN 3-540-64589-6. pp 57-97 (1999).

[2] Aczel, P. On relating type theories and set theories, in Types `98, the proceedings of the 1998 workshop on Types for Proofs and Programs, at Kloster Irsee, edited by T. Altenkirch, W. Naraschewski and B. Reus, Springer Lecture Notes in Computer Science, LNCS 1657, pp 1-18 (1999).

[3] Aczel, P. The Russell-Prawitz Modality, SUBMITTED to Mathematical Structures in Computer Science, (1999).

[4] Bailey, A. The machine-checked literate formalisation of algebra in type theory, Ph.D. thesis, Manchester University, (1999).

[5] Gambino, N. Types and Sets: a study on the jump to full impredicativity, Lauria Thesis, Padua University, (1999).

Next: University of Oxford Up: Progress Report Previous: University of Helsinki