Birkedal, Lars and Møgelberg, Rasmus E. and Petersen, Rasmus Lerchedahl - Linear Abadi and Plotkin Logic

lmcs:2233 - Logical Methods in Computer Science, November 3, 2006, Volume 2, Issue 5
Linear Abadi and Plotkin Logic

Authors: Birkedal, Lars and Møgelberg, Rasmus E. and Petersen, Rasmus Lerchedahl

We present a formalization of a version of Abadi and 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' 1995 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.


Source : oai:arXiv.org:cs/0611004
DOI : 10.2168/LMCS-2(5:2)2006
Volume: Volume 2, Issue 5
Published on: November 3, 2006
Submitted on: April 20, 2006
Keywords: Computer Science - Logic in Computer Science,F.4.1,D.3.3


Share

Consultation statistics

This page has been seen 71 times.
This article's PDF has been downloaded 19 times.