Fully Complete Models for ML Polymorphic Types

Samson Abramsky and Marina Lenisa


We present an axiomatic characterization of models fully-complete for ML-polymorphic types of System F. This axiomatization is given for hyperdoctrine models, which arise as adjoint models, i.e. co-Kleisli categories of suitable linear categories. Examples of adjoint models can be obtained from categories of Partial Equivalence Relations over Linear Combinatory Algebras. We show that a special linear combinatory algebra of partial involutions induces an hyperdoctrine which satisfies our axiomatization, and hence it provides a fully-complete model for ML-types.


This report is available in the following formats:

Previous | Index | Next