Abstract of Paper

Axiomatizing Fully Complete Models for ML Polymorphic Types
by Samson Abramsky and Marina Lenisa


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