A characterization of lambda definability in categorical models of implicit polymorphism

AbstractLambda 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