A Logic for Parametric Polymorphism
| Author(s) : | Gordon Plotkin, |
| Publisher : | N/A |
| Publication Date : | 1993 |
| ISSN : | N/A |
| 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. 1, |