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 (Tech. Report, University of Turin, 1997), hence it contains complete models for Fη (A βη-complete model for system F, preprint, June, 1998) and we conjecture that it contains models which are complete for F. It also contains simpler models, the simplest of them, Image, being a second-order variant of the Engeler–Plotkin model Image. 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 Berline (From computations to foundations: the λ-calculus and its webbed models, revised version, Theoret. Comput. Sci. 86 pp., to appear)), but it is much larger than this. Finally, many of its models might be read as two intertwined strict intersection type systems.

Building Continuous Webbed Model for system F

BERARDI, Stefano;
2004-01-01

Abstract

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 (Tech. Report, University of Turin, 1997), hence it contains complete models for Fη (A βη-complete model for system F, preprint, June, 1998) and we conjecture that it contains models which are complete for F. It also contains simpler models, the simplest of them, Image, being a second-order variant of the Engeler–Plotkin model Image. 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 Berline (From computations to foundations: the λ-calculus and its webbed models, revised version, Theoret. Comput. Sci. 86 pp., to appear)), but it is much larger than this. Finally, many of its models might be read as two intertwined strict intersection type systems.
2004
315
3
34
S. BERARDI; C. BERLINE
File in questo prodotto:
File Dimensione Formato  
Building Continuous Webbed Model for system F.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 408.08 kB
Formato Adobe PDF
408.08 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/41573
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact