School of Computer Science
University of Birmingham
2pm, Friday 11 February 2005
Room 2511, JCMB, King's Buildings
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.