This is to advertise the monograph "Synthetic topology of data types and classical spaces" http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf (or dvi or ps) which will appear soon in volume 83 of ENTCS. NB. (1) For those of you who attended my PSSL talk in Cambridge: The topos-theoretic treatment of synthetic topology has not been included here. (2) This monograph supersedes a preliminary version which was previously available from my web page. Martin Escardo -- Summary (not as in the monograph) This monograph consists of three parts divided in 6+5+2 chapters. Part II (topology of classical spaces) applies the exponential law for function spaces, with the aid of the Sierpinski space, to develop the core of classical topology in a transparent (and constructive) way. Mathematicians can start from this part, and even confine their attention to it. Part I (topology of data types) emulates the second and stands on its own. It starts from the well known ideas that (1) the Sierpinski space plays the role a data type of results of semidecisions or observations, and (2) the notion of continuous map has that of computable or programmable map as a computational counterpart. The development of the synthetic topology of data types offered in this part is operational rather than denotational. This is to emphasize that the topology is there, even in the case of sequential programming languages, independently of which denotational model one favours (if any). Part III starts by unifying the first and the second, again following well known ideas, and then develops further applications to computation, this time with the aid of denotational semantics. In particular, the Tychonoff theorem for countably many factors is invoked to establish termination of a certain program (in the simply-typed lambda calculus with natural numbers and fixed-point recursion). In turn, termination of the program implies the Tychonoff theorem for countably many second countable compact spaces. ------------------------------------------------------------------------ http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf ------------------------------------------------------------------------
participants (1)
-
Martin Escardo