Personal tools
You are here: Home Events Abstract Archives 2005 Operational Domain Theory and Topology of a Sequential Programming Language

Operational Domain Theory and Topology of a Sequential Programming Language

Martin 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 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.

Document Actions