Loading...
Please wait, while we are loading the content...
Similar Documents
The Genericity Theorem and the Notion of Parametricity in the Polymorphic λ-calculus
| Content Provider | Semantic Scholar |
|---|---|
| Author | Longo, Giuseppe Milsted, Kathleen Soloviev, Sergei |
| Copyright Year | 1992 |
| Abstract | This paper focuses on how terms of second order λ-calculus, which may take types as inputs, depend on types. These terms are generally understood to have an “essentially” constant meaning, in all models, on input types. We show how the proof theory of second order λ-calculus suggests a clear syntactic description of this phenomenon. Namely, under a reasonable condition, we show that identity of two polymorphic functions on a single type implies identity of the functions (equivalently, every type is a generic input). |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.hpl.hp.com/techreports/Compaq-DEC/PRL-RR-21.pdf |
| Alternate Webpage(s) | http://www.di.ens.fr/users/longo/files/genericity-theorem.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
