Alpha-Conversion and Typability

There are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-orderλ-calculusFof 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λ-calculusF ω of Girard, by exhibiting a term which is typable inF ω with alpha-conversion but not typable inF ω without alpha-conversion.

Authors

• A.J. Kfoury
• S. Ronchi della Rocca
• J. Tiuryn
• P. Urzyczyn

Keywords

No keywords are indexed for this paper.