Linear Abadi and Plotkin Logic
Lars Birkedal, Rasmus E. M{\o}gelberg, Rasmus Lerchedahl, Petersen

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
