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.
Publications
[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