Abstract Stone Duality is a reaxiomatisation of general topology that is intended to unify it with recursion theory and translate topological constructions into executable programs. In a sense, it turns denotational semantics on its head: from topology (not just domain theory) to programs. The underlying idea is Pare's theorem, that the category of "frames" is both dual to and monadic over the category of "spaces". The leading concrete examples are * the category of locally compact locales and * any elementary topos, so - unlike existing programming languages and formal type theories - there are "subtypes", which can be carved out by means of something like the axiom of comprehension in set theory. Unfortunately the subject is not yet in a state where I can give an introduction suitable for either topologists or computer scientists: I am still building basic categorical structure on the central hypothesis, and familiarity with Beck's theorem that characterises monadic adjunction is essential at this stage. This is just an interim progress report for those that already know a little about this work. Links to the published and draft papers are at http://www.dcs.qmw.ac.uk/~pt/ASD or http://hypatia.dcs.qmw.ac.uk/author/TaylorP In particular, the paper that I presented at CT2000 in Como, Non-Artin Gluing in Recursion Theory and Lifting in Abstract Stone Duality recently came back from the referees and has now been revised. If you have any comments on this paper, please tell me now so that they can be incorporated in the revised version. It contains a counterexample to show that the Artin comma square for recovering the topology on a space from the topologies of an open subspace and its closed complement does not work for the analogous lattices of recursively enumerable subsets of N, considered as Godel numbers for terminating and non-terminating programs. However, it analyses the gluing problem a little further, and shows that the modular law for lattices plays an important part. On this is built the construction of the partial map classifier in abstract Stone duality. The paper follows and relies heavily on Geometric and Higher Order Logic in Abstract Stone Duality, which was published in Theory and Applications of Categories in Dec 2000. For the past few months I have been working on (the category theory and) a lambda calculus for the monadic principle that underlies ASD. This was presented at the APPSEM workshop in Darmstadt in March. I was hoping to have it in a releasable state by now, but, as usual, the paper grew much too big, so I split it in two, so it lost its narrative structure. I hope to be able to release a draft of that later in the summer. The main job for the summer is to get working a prototype compiler that I started writing last summer, to translate from my comprehension-like lambda calculus into pure PROLOG. The reason for choosing PROLOG is that its semantics is (amongst existing programming languages) closest to the semantic ideas in ASD. Paul