Paper: Kripke-Style models for typed lambda calculus (at LICS 1987)

Authors: John C. Mitchell Eugenio Moggi

Abstract

The semantics of typed lamda calculus is usually described using classical models, consisting of set-theoretic functions over some ground domains, or cartesian closed categories. We discuss Kripke-style models which are more general than classical models, and may be regarded as "semantic" but not nessarily concrete cartesian closed categories. We show that the traditional inference system, while incomplete for classical models which may have empty types, is complete for Kripke models. Furthermore, in contrast to the classical situation, every set of equations that is closed under semantic implication is the theory of a single model. We also develop some properties of logical relations over Kripke structures, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a classical lambda model.

BibTeX

  @InProceedings{MitchellMoggi-KripkeStylemodelsfo,
    author = 	 {John C. Mitchell and Eugenio Moggi},
    title = 	 {Kripke-Style models for typed lambda calculus},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {303--314},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }