ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Subtyping and parametricity (at LICS 1994)

Authors: Gordon D. Plotkin Martín Abadi Luca Cardelli


We study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal definition and use of relational parametricity. We give two models for it, and compare it with other formal systems for the same language. In particular we examine the “Penn interpretation” of subtyping as implicit coercion. without subtyping, parametricity yields, for example, an encoding of abstract types and of initial algebras, with the corresponding proof principles of simulation and induction. With subtyping, we obtain partially abstract types and certain initial order-sorted algebras, and may derive proof principles for them


    author = 	 {Gordon D. Plotkin and Martín Abadi and Luca Cardelli},
    title = 	 {Subtyping and parametricity},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {310--319},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton