The Genericity Theorem and effective Parametricity in Polymorphic lambda-calculus - ENS - École normale supérieure Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 1993

The Genericity Theorem and effective Parametricity in Polymorphic lambda-calculus

Kathleen Milsted
  • Fonction : Auteur
Sergei Soloviev

Résumé

This paper focuses on how terms of the polymorphic λ-calculus, which may take types as inputs, depend on types. These terms are generally understood, in all models, to have an “essentially” constant meaning on input types. We show the proof theory of polymorphic λ-calculus suggests a clear syntactic description of this phenomenon. Namely, under a reasonable condition, we show that if two polymorphic functions agree on a single type, then they agree on all types (equivalently, types are generic inputs).
Fichier principal
Vignette du fichier
2021_08_10_genericity-theorem.pdf (181.21 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03316293 , version 1 (10-08-2021)

Identifiants

Citer

Giuseppe Longo, Kathleen Milsted, Sergei Soloviev. The Genericity Theorem and effective Parametricity in Polymorphic lambda-calculus. Theoretical Computer Science, 1993, 121 (1-2), pp.323-349. ⟨10.1016/0304-3975(93)90093-9⟩. ⟨hal-03316293⟩
38 Consultations
34 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More