An axiomatic system of parametricity

• Autorzy: Takeuti I.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

parametricity; polymorphism; lambda calculus

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1998
• Tom: Vol. 33, nr 4
• Strony: 397--432
• Opis fizyczny: bibliogr. 9 poz.

Twórcy

autor

Takeuti I.

• Department of Information Science Kyoto University Kyoto, 606-8501 Japan,