A Logic for Parametric Polymorphism
View/ Open
Date
05/11/2003Author
Plotkin, Gordon
Abadi, Martin
Metadata
Abstract
In this paper we introduce a logic for parametric polymorphism. Just as LCF is a
logic for the simply-typed -calculus with recursion and arithmetic, our logic is a logic for
System F. The logic permits the formal presentation and use of relational parametricity.
Parametricity yields—for example—encodings of initial algebras, final co-algebras and
abstract datatypes, with corresponding proof principles of induction, co-induction and
simulation.