Paper: Polymorphism, set theory, and call-by-value (at LICS 1990)

Authors: Edmund P. Robinson Giuseppe Rosolini

Abstract

Set-theoretic (or rather the more general topos-theoretic) models of polymorphic lambda-calculi are discussed under the assumption that the datatypes of the language are to be interpreted as sets and the operations as partial functions. It is shown that it is not possible to obtain a model in which function spaces are interpreted by the full partial function space, but that it is nevertheless possible to have models which incorporate a usefully large class of partial functions. The main result is that set-theoretic models do not exist, even constructively. This is a much stronger result than holds for the classical sound-order lambda calculus

BibTeX

  @InProceedings{RobinsonRosolini-Polymorphismsettheo,
    author = 	 {Edmund P. Robinson and Giuseppe Rosolini},
    title = 	 {Polymorphism, set theory, and call-by-value},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {12--18},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }