• DocumentCode
    2023444
  • Title

    Operational domain theory and topology of a sequential programming language

  • Author

    Escardó, Martín ; Kin, Ho Weng

  • Author_Institution
    Sch. of Comput. Sci., Univ. of Birmingham, UK
  • fYear
    2005
  • fDate
    26-29 June 2005
  • Firstpage
    427
  • Lastpage
    436
  • 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.
  • Keywords
    programming language semantics; programming theory; reasoning about programs; denotational semantics; operational domain theory; program correctness proving; sequential programming language; Computer languages; Computer science; Context modeling; Finite element methods; Game theory; Logic; Topology; Virtual manufacturing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-2266-1
  • Type

    conf

  • DOI
    10.1109/LICS.2005.34
  • Filename
    1509248