Building continuous webbed models for System F
Berardi, Stefano ; Berline, Chantal
HAL, hal-00003750 / Harvested from HAL
We present here a large family of concrete models for Girard and Reynolds polymorphism (System F), in a noncategorical setting. The family generalizes the construction of the model of Barbanera and Berardi, hence it contains models which are complete for F. It also contains simpler models, the simplest of them, E², being a second-order variant of the Engeler-Plotkin model E. All the models here belong to the continuous semantics, all have the maximum number of polymorphic maps. The class contains models which can be viewed as two intertwined compatible webbed models of untyped lambda-calculus, but is much larger than this. Finally many of its models might be read as two intertwined strict intersection type systems.
Publié le : 2004-07-05
Classification:  lambda-calculus,  continuous semantics,  polymorphism,  polymax models,  webbed models,  MSC: 03B40, 03B70,  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
@article{hal-00003750,
     author = {Berardi, Stefano and Berline, Chantal},
     title = {Building continuous webbed models for System F},
     journal = {HAL},
     volume = {2004},
     number = {0},
     year = {2004},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00003750}
}
Berardi, Stefano; Berline, Chantal. Building continuous webbed models for System F. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00003750/