Logic in Computer Science (LICS 1988)

Paper: The topology of program termination (at LICS 1988)

Authors: Robert Cartwright Alan J. Demers

Abstract

Denotational semantics is founded on a theory of higher order computation called domain theory, which formalizes a computation as a potentially infinite enumeration of finite elements that approximate the answer with progressively higher accuracy. Although existing formulations of domain theory provide an elegant framework for defining the abstract meaning of programs, these definitions are not effective because they fail to specify when computations terminate. A formulation of domain theory is presented that gives a natural topological characterization of termination: the evaluation of a program expression should terminate if and only if the expression denotes an element that is finite and maximal

BibTeX

  @InProceedings{CartwrightDemers-Thetopologyofprogra,
    author = 	 {Robert Cartwright and Alan J. Demers},
    title = 	 {The topology of program termination},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {296--308},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }