ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

Authors: Edmund P. Robinson Giuseppe Rosolini


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


    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}

Last modified: 2022-10-3113:49
Sam Staton