Axiomatizing Fully Complete Models for ML Polymorphic Types

Abstract We present axioms on models of system F, which are sufficient to show full completeness for ML-polymorphic types. These axioms are given for hyperdoctrine models, which arise as adjoint models, i. e. co-Kleisli categories of linear categories. Our axiomatization consists of two crucial steps. First, we axiomatize the fact that every relevant morphism in the model generates, under decomposition, a possibly infinite typed Böhm tree. Then, we introduce an axiom which rules out infinite trees from the model. Finally, we discuss the necessity of the axioms.

Authors

• Samson Abramsky
• Marina Lenisa

Keywords

No keywords are indexed for this paper.