A Fully Complete PER Model for ML Polymorphic Types

Abstract We present a linear realizability technique for building Partial Equivalence Relations (PER) categories over Linear Combinatory Algebras. These PER categories turn out to be linear categories and to form an adjoint model with their co-Kleisli categories. We show that a special linear combinatory algebra of partial involutions, arising from Geometry of Interaction constructions, gives rise to a fully and faithfully complete model for ML polymorphic types of system F.

Authors

• Samson Abramsky
• Marina Lenisa

Keywords

No keywords are indexed for this paper.