
Operational Domain Theory and Topology of a Sequential Programming LanguageMartin Escardo 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 sidestepping denotational semantics and reformulating domaintheoretic and topological notions directly in terms of programming concepts, interpreted in an operational way. We apply this to prove the correctness of nontrivial (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. Document Actions 
