Linear Abadi and Plotkin Logic

@misc{citeulike:925601, abstract = {We present a formalization of a version of Abadi and <br />Plotkin's logic for parametricity for a polymorphic dual intuitionistic / linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction / coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of ``admissible'' relations. A similar property was observed in Pitts analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models.}, author = {Birkedal, Lars and M\&oslash;gelberg, Rasmus E. and Petersen, Rasmus L. }, citeulike-article-id = {925601}, eprint = {cs/0611004}, keywords = {coinduction, linear-logic, programming-logic, recursive-types}, month = {Nov}, posted-at = {2006-11-02 13:52:04}, priority = {2}, title = {Linear Abadi and Plotkin Logic}, url = {http://arxiv.org/abs/cs/0611004}, year = {2006} }

TY - ELEC ID - citeulike:925601 L3 - citeulike-article-id:925601 TI - Linear Abadi and Plotkin Logic N2 - We present a formalization of a version of Abadi and <br />Plotkin's logic for parametricity for a polymorphic dual intuitionistic / linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction / coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of ``admissible'' relations. A similar property was observed in Pitts analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models. KW - coinduction KW - linear-logic KW - programming-logic KW - recursive-types AU - Birkedal, Lars AU - M&oslash;gelberg, Rasmus AU - Petersen, Rasmus PY - 2006/Nov/01/ UR - http://arxiv.org/abs/cs/0611004 ER -