Peter Aczel has been investigating issues concerning the development of formal topology in Martin-Lof's type theory. An alternative to the direct treatment of formal topology in type theory is to work in constructive axiomatic set theory and exploit Aczel's earlier translation of the set theory into the type theory. An important issue is the role of generalised inductive definitions in formal topology. The investigation of this topic has led to a `compactness' result about generalised inductive definitions in the predicative context of Martin-Lof's type theory or alternatively of constructive axiomatic set theory. This work also raises again the possibility that a computer implementation of constructive axiomatic set theory may be a worthwhile approach to developing machine checked constructive mathematics.
In the period Aczel has made short visits to Padua to discuss formal topology and generalised inductive definitions and planned a longer visit for 1997-98. He attended the WG Aussois workshop and gave a series of lectures on constructive type theory at the 1997 Marktoberdorf international summer school. He is also planning to write and lecture on constructive axiomatic set theory in 1997-98.
Anthony Bailey has been working on ways to present formal mathematics in a more readable style closer to that seen in informal accounts. He is planning to submit his PhD thesis, which is centred around a so-called "literate formalisation" of some Galois theory, in December 1997. Part of that work involved implementing a system for implicit coercions within LEGO, and he talked on the matters that arose in the process of doing this at Aussois; a paper "Coercion synthesis in computer implementations of type-theoretic frameworks" has been submitted for the proceedings. He also attended the Durham workshop.