[Prev][Next][Index][Thread]
Lambda Definability in Categorical Models
A Characterization of Lambda Definability
in Categorical Models of Implicit Polymorphism
Moez Alimohamed
University of Pennsylvania
This paper contains the work of Moez Alimohamed, a mathematics graduate
student at the University of Pennsylvania who died tragically on August 29th.
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 characterization of
lambda definability in Henkin models for the simply typed lambda calculus
first to ccc models, and then to categorical models of the calculus with
type variables.
WWW access is http://www.cis.upenn.edu/~andre/moez.html. The paper is also
available by anonymous ftp from the host ftp.cis.upenn.edu as the file
pub/papers/scedrov/def.ps.Z.