Sciweavers

TLCA
1993
Springer

A Logic for Parametric Polymorphism

14 years 3 months ago
A Logic for Parametric Polymorphism
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 datatypes, with corresponding proof principles of induction, co-induction and simulation.
Gordon D. Plotkin, Martín Abadi
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1993
Where TLCA
Authors Gordon D. Plotkin, Martín Abadi
Comments (0)