Building continuous webbed models for system F

8 years 10 months ago
Building continuous webbed models for system F
We present here a large family of concrete models for Girard and Reynolds polymorphism (System F), in a non categorical setting. The family generalizes the construction of the model of Barbanera and Berardi [2], hence it contains complete models for F [5] and we conjecture that it contains models which are complete for F. It also contains simpler models, the simplest of them, E2 , being a second order variant of the Engeler-Plotkin model E. All the models here belong to the continuous semantics and have underlying prime algebraic domains, all have the maximum number of polymorphic maps. The class contains models which can be viewed as two intertwined compatible webbed models of untyped -calculus (in the sense of [8]), but it is much larger than this. Finally many of its models might be read as two intertwined strict intersection type systems. Contents
Stefano Berardi, Chantal Berline
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Authors Stefano Berardi, Chantal Berline
Comments (0)