Domain theoretic models of polymorphism (Q1824612)

The authors present a category-theoretic model for polymorphic lambda- calculus. Types are interpreted as Scott domains and types with free type variables as functors on domains. The paper emphasizes the important role Grothendieck fibrations and continuous sections play in the interpretation of polymorphism. The approach is based on examples, many particular constructions are presented so that the ideas are concretely expressed. Finally, the paper presents interesting questions and comparisons with other models for polymorphism.