Domain theory and topology in programming language semantics have been applied to manufacture and study denotational models, e.g., the Scott model of PCF. As is well known, for a sequential language like this, the match of the model with the operational semantics is imprecise: computational adequacy holds but full abstraction fails.

The main achievement of the present work is a reconciliation of a good deal of domain theory and topology with sequential computation. This is accomplished by side-stepping denotational semantics and reformulating domain-theoretic and topological notions directly in terms of programming concepts, interpreted in an operational way.

We apply this to prove the correctness of non-trivial (but short) programs that manipulate infinite data, in particular real numbers represented as infinite sequences of digits.

This is joint work with Ho Weng Kin.