[For the entire collection see Zbl 0635.00016.]
From the authors’ introduction: “There has been considerable interest recently... for polymorphic types... The current syntactic paradigm for polymorphic typing is higher-order lambda calculus, for which there are no nontrivial set-theoretic interpretations. In a recent work of Moggi & Hyland, however, a recursive interpretation of polymorphic types obtained by Girard is inferred within the setting for an intuitionistic theory of sets given by the Realizability Universe... We consider a different approach based on a calculus of relations that allows us to show that the recursive functions and realizability are in fact forced by the required higher-order logical structure of the category in question. Various new interpretations of polymorphism... are then easily obtaind... The method itself and the basic results are explained here...”