Logic in Computer Science (LICS 1988)

Paper: Can LCF be topped? Flat lattice models of typed lambda calculus (at LICS 1988)

Authors: Bard Bloom

Abstract

G. Plotkin (1977) examined the denotational semantics of LCF (essentially typed lambda calculus with arithmetic and looping). He showed that the standard Scott semantics is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an extential operator, denotationally universal. This treatment is extended to Scott models built from flat lattices rather than flat cpo's. It is found that no extension of LCF can be denotationally universal. A fully abstract extension based on Godel numbering and synthetic analysis is the best that can be achieved. Operators defined by LCF-style rules cannot give fully abstract language. It is shown that Plotkin's program can be carried out for a nonconfluent evaluator

BibTeX

  @InProceedings{Bloom-CanLCFbetoppedFlatl,
    author = 	 {Bard Bloom},
    title = 	 {Can LCF be topped? Flat lattice models of typed lambda calculus},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {282--295},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }