@MISC{PCS_0.MIZ,
  AUTHOR = {Grue, Klaus E. and Korni{\l}owicz, Artur},
  NOTE2 = {The author visited Dept. Comp. Sci., Univ.of Copenhagen. while writing the article},
  TITLE = {Basic Operations on Preordered Coherent Spaces},
  ACKNOWLEDGEMENT = {The authors would like to thank DIKU (dept.comp.sci., univ.of Copenhagen)
    and the FIRST Research School for hosting the second author in Copenhagen
    and funding the cooperation which led to the present Mizar paper.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Relational Structures},
  SECTION3 = {Tolerance Structures},
  SECTION4 = {PCS's},
  DAY = {28},
  MONTH = {August},
  YEAR = {2007},
  ADDRESS1 = {DIKU\\University of Copenhagen\\Universitetsparken 1\\DK-2100 Copenhagen\\Denmark},
  ADDRESS2 = {Institute of Computer Science\\University of Bia{\l}ystok\\Sosnowa 64, 15-887 Bia{\l}ystok\\Poland},
  SUMMARY = {This Mizar paper presents the definition of a 'Preordered Coherent Space'
   (PCS). Furthermore, the paper defines a number of operations on PCSs and
   states and proves a number of elementary lemmas about these operations.
   PCSs have many pleasing properties which could qualify them for mathematical
   study in their own right. PCSs were invented, however, to construct Scott
   domains, to solve domain equations, and to construct models of various
   versions of lambda calculus.\par
  For more on PCSs, see \cite{Krivine}.
  The present Mizar paper defines the operations on PCSs
  used in Chapter 8 of \cite{berline97kappadenotational}.}}


