It is known from various lines of attack (intuitionistic and constructive mathematics, recursion theory, domain theory, programming language semantics, type-two theory of effectivity) that domains of computation, or data types, are topological spaces, and that computable maps are continuous. Moreover, the topologies that arise are familiar. For instance, computable functions on infinite sequences of binary digits are continuous with respect to the Cantor topology. Many applications of the topology of data types are known in the theory of computation. To give a simple example, it follows from the compactness of the Cantor space that equality of integer-valued predicates on the Cantor space is decidable.
We approach this from what we call \emph{synthetic topology}. The idea is to define topological notions (such as continuous map, open set, discrete space, Hausdorff space, compact space) by means of familiar computational concepts (computable function, semidecidable set, set with semidecidable equality, set with semidecidable apartness, set over which one can universally quantify by computational means), and prove topological theorems about them by computational means. For example: (1) Compactness of the Cantor space is proved by constructing a program for universally quantifying over it. (2) The theorem that a compact subspace $Q$ of a Hausdorff space $X$ is closed has the following computational manifestation: If we can computationally tell distinct points of $X$ apart and we can computationally quantify over $Q$, then we can computationally semidecide the complement of $Q$. The proof is the evident algorithm that defines the semidecision function for the complement of $Q$ from the apartness map of $X$ by universally quantifying over $Q$.
At a later stage, we convince ourselves that both the synthetic definitions and the computational proofs match the classical topological ones. In fact, after having developed synthetic topology, we turn the programme on its head: We show that one can cheaply develop the core of classical topology via the lambda-calculus.
See Martin's paper Topology of data types, the course will cover Chapters 1-5, and some bits of Chapter 12.