Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >
Please use this identifier to cite or link to this item:
|Title: ||A Logic for Parametric Polymorphism|
|Authors: ||Plotkin, Gordon|
|Issue Date: ||5-Nov-2003|
|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
|Keywords: ||Laboratory for Foundations of Computer Science|
|Appears in Collections:||Informatics Publications|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.