| |
VOLUME 2, ISSUE 5, PAPER 2
|
Linear Abadi and Plotkin Logic
|
©Lars Birkedal, IT University of Copenhagen
©Rasmus E. Møgelberg
©Rasmus Lerchedahl Petersen
|
Abstract
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.
|
Publication date: November 3, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(5:2)2006
Hit Counts: 3920 |
 Creative Commons | |
