Name
Abstract | ||
|---|---|---|
There are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-order λ -calculus F of Girard and Reynolds without affecting the typing power of the system. On the other hand we show that it is impossible to eliminate alpha-conversion on universally quantified variables in the higher-order λ -calculus F ω of Girard, by exhibiting a term which is typable in F ω with alpha-conversion but not typable in F ω without alpha-conversion. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1006/inco.1998.2756 | Inf. Comput. |
Field | DocType | Volume |
Lambda calculus,Calculus,Mathematics | Journal | 150 |
Issue | ISSN | Citations |
1 | Information and Computation | 3 |
PageRank | References | Authors |
0.43 | 7 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| A. J. Kfoury | 1 | 461 | 47.34 |
| S. Ronchi della Rocca | 2 | 43 | 3.32 |
| Jerzy Tiuryn | 3 | 229 | 22.79 |
| P. Urzyezyn | 4 | 3 | 0.43 |