Linear Abadi and Plotkin Logic

TL;DR

This paper formalizes a logic for parametricity in a polymorphic dual intuitionistic/linear type theory, enabling the definition and reasoning about complex types like recursive, existential, inductive, and coinductive types.

Contribution

It introduces a formal logic for parametricity in a polymorphic linear type theory, allowing the construction and reasoning of advanced types including recursive and inductive types.

Findings

Recursive types satisfy dinaturality property.

Develops mixed induction/coinduction reasoning principles.

Coinduction applies to all relations, induction limited to admissible relations.

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.