  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.
