Alpha-Conversion and Typability

Author： Kfoury A.J.   Ronchi della Rocca S.   Tiuryn J.   Urzyczyn P.  

Publisher： Academic Press

ISSN： 0890-5401

Source： Information and Computation, Vol.150, Iss.1, 1999-04, pp. : 1-21

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

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. Copyright 1999 Academic Press.

Related content

Conversion of Phthalimides to Isoindolines by Diborane

By Strassert Cristian A.   Awruch Josefina  

Monatshefte für Chemie / Chemical Monthly, Vol. 137, Iss. 12, 2006-12 ,pp. : 1499-1503 (5)

Springer Publishing Company

Access to resources Recommend Favorite

The Chemistry of Energy Conversion and Storage

By  

CHEMSUSCHEM (ELECTRONIC) CHEMISTRY AND SUSTAINABILITY, ENERGY & MATERIALS, Vol. 7, Iss. 5, 2014-05 ,pp. : 1199-1200 (2)

John Wiley & Sons Inc

Access to resources Recommend Favorite

Solution to A Base Conversion Surprise

By  

American Mathematical Monthly, Vol. 122, Iss. 4, 2015-04 ,pp. : 402-402 (1)

Mathematical Association of America

Access to resources Recommend Favorite

A Base Conversion Surprise

By Ponomarenko Vadim  

American Mathematical Monthly, Vol. 122, Iss. 4, 2015-04 ,pp. : 366-366 (1)

Mathematical Association of America

Access to resources Recommend Favorite

The scattering of nucleons by alpha-particles

By Hodgson P.E.  

Advances In Physics, Vol. 7, Iss. 25, 1958-01 ,pp. : 1-39 (39)

Taylor & Francis Ltd

Access to resources Recommend Favorite