Logic in Computer Science (LICS 2002)

Paper: Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (at LICS 2002)

Authors: Alex Simpson

Abstract

We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. Our method of construction is to obtain such models as full subcategories of categorical models of intuitionistic set theory. We show that the existence of solutions to recursive domain equations, needed for the interpretation of recursive types, depends on the strength of the set theory. The internal set theory of an elementary topos is not strong enough to guarantee their existence. However, using models of intuitionistic Zermelo-Fraenkel set theory instead, we prove an algebraic compactness result. We apply this to obtain an interpretation of FPC in any model. Lastly, we provide necessary and sufficient conditions on a model for the interpretation to be computationally adequate, i.e. for the operational and denotational notions of convergence to agree.

BibTeX

  @InProceedings{Simpson-ComputationalAdequa,
    author = 	 {Alex Simpson},
    title = 	 {Computational Adequacy for Recursive Types in Models of
    Intuitionistic Set Theory},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }