Logic in Computer Science (LICS 2005)

Paper: Operational Domain Theory and Topology of a Sequential Programming Language (at LICS 2005)

Authors: Martin Escardo Ho Weng Kin

Abstract

A number of authors have exported domain-theoretic techniques from denotational semantics to the operational study of contextual equivalence and preorder. We further develop this, and, moreover, we additionally export topological techniques. In particular, we work with an operational notion of compact set and show that total programs with values on certain types are uniformly continuous on compact sets of total elements. We apply this and other conclusions to prove the correctness of non-trivial programs that manipulate infinite data. What is interesting is that the development applies to sequential programming languages.

BibTeX

  @InProceedings{EscardoKin-OperationalDomainTh,
    author = 	 {Martin Escardo and Ho Weng Kin},
    title = 	 {Operational Domain Theory and Topology of a Sequential Programming Language},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {427--436},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }