Paper announcement

The following paper is now available over the Web.

           Computational Adequacy for Recursive Types
             in Models of Intuitionistic Set Theory

  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. This allows us to obtain a notion of model that encompasses
  both domain-theoretic and realizability models. 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, solutions 
  to recursive domain equations do exist if models of intuitionistic
  Zermelo-Fraenkel set theory are used instead. We apply this result
  to interpret FPC, and 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 termination 
  to agree.



Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: Alex.Simpson@dcs.ed.ac.uk             Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als                Fax: +44 (0)131 667 7209  
URL: http://www.dcs.ed.ac.uk/home/als