Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

The Genericity Theorem and effective Parametricity in Polymorphic lambda-calculus

Abstract : 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).
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-ens.archives-ouvertes.fr/hal-03316293
Contributeur : Usr 3608 République Des Savoirs <>
Soumis le : mardi 10 août 2021 - 15:59:24
Dernière modification le : mercredi 11 août 2021 - 03:02:21

Fichier

2021_08_10_genericity-theorem....
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

23

Téléchargements de fichiers

9