A characterization of lambda definability in categorical models of implicit polymorphism
Moez Alimohamed · Theoretical Computer Science · 1995
Lambda definability is characterized in categorical models of simply typed lambda calculus with type variables. A category-theoretic framework known as glueing or sconing is used to extend the Jung-Tiuryn (1993) characterization of lambda definability first to ccc models, and then to categorical models of the calculus with type variables.