Search

• < Previous
• 1
• Next >

Linear Abadi and Plotkin Logic

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,&nbsp;[&hellip;]