A logic for parametric polymorphism Export

@inproceedings{citeulike:1224724, 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 Introduction In this paper we introduce a...}, address = {Utrecht, The Netherlands}, author = {Plotkin, Gordon and Abadi, Mart\'\in}, booktitle = {International Conference on Typed Lambda Calculi and Applications}, citeulike-article-id = {1224724}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7987}, editor = {Bezem, M. and Groote, J. F.}, keywords = {logic, polymorphism, system-f}, number = {664}, pages = {361--375}, posted-at = {2007-04-14 04:02:58}, priority = {2}, publisher = {Springer-Verlag}, title = {A logic for parametric polymorphism}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7987}, year = {1993} }

TY - CONF ID - citeulike:1224724 L3 - citeulike-article-id:1224724 N2 - 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 Introduction In this paper we introduce a... IS - 664 AD - Utrecht, The Netherlands EP - 375 TI - A logic for parametric polymorphism PB - Springer-Verlag T2 - International Conference on Typed Lambda Calculi and Applications SP - 361 KW - logic KW - polymorphism KW - system-f AU - Plotkin, Gordon AU - Abadi, Mart\'\in A2 - Bezem, M A2 - Groote, JF PY - 1993/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7987 ER -