Lambda Definability in Categorical Models

• To: types@dcs.gla.ac.uk, categories@mta.ca
• Subject: Lambda Definability in Categorical Models
• From: andre@saul.cis.upenn.edu (Andre Scedrov)
• Date: Tue, 11 Oct 1994 18:02:14 -0400
• Approved: types@dcs.gla.ac.uk

               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.  

• Prev: Paper announcement
• Next: LLL
• Index(es):
  • Main
  • Thread