Abstract
In this paper we consider “powerset models” of the non-extensional typed lambda calculus. Although the interpretation of the type constructor ⇒ is in general not uniquely determined, we can make a canonical choice in this particular ase; there exists a minimal interpretation of ⇒ (with respect to a certain class of interpretations) which yields models with a maximal theory (in that class).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Gunther, C. A., Comparing Categories of Domains, in: A. Melton (Ed.), Mathematical Foundations of Programming Semantics, Proceedings Int. Conference 1985, Lect. Notes in Comp. Sci., vol. 239, Springer-Verlag, Berlin, 1986, pp. 101–121.
Hayashi, S., Adjunction of Semifunctors: Categorical Structures in Non-Extensional Lambda-Calculus, Theor. Comput. Sci. 41 (1985), 95–104.
Hoofman, R., The Theory of Semi-Functors, Mathematical Structures in Computer Science, 3 (1993), 93–128.
Plotkin, G. D., Set-Theoretical and other Elementary Models of the λ-calculus, Theoretical Computer Science, 121 (1993), 351–409.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoofman, R. (1994). Comparing models of the non-extensional typed λ-calculus extended abstract. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_17
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive