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 Bohm tree. Then, we introduce an axiom which rules out infinite trees from the model. Finally, we discuss the necessity of the axioms.