An Axiomatic System of Parametricity

Article type: Research Article

Authors: Takeuti, Izumi

Affiliations: Department of Information Science, Kyoto University, Kyoto, 606-8501 Japan. [email protected]

Abstract: Plotkin and Abadi have proposed a syntactic system for parametricity based on a second order predicate logic. This paper shows three theorems about that system. The first is consistency of the system, which is proved by the method of relativization. The second is that polyadic parametricities of recursive types are equivalent to each other. The third is that the theory of parametricity for recursive types is self-realizable. As a corollary of the third theorem, the theory of parametricity for recursive types satisfies the term extraction property.

Keywords: parametricity, polymorphism, typed lambda calculus

DOI: 10.3233/FI-1998-33404

Journal: Fundamenta Informaticae, vol. 33, no. 4, pp. 397-432, 1998