Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus. However he later showed that this approach was inconsistent with classical set theory. Pitts described the framework of hyperdoctrine models and topos models which are consistent with constructive logic.
Presumably relational hyperdoctrine and topos models were then developed. Where can I read about them?
-  Types, abstraction and parametric polymorphism
-  Polymorphism is not set-theoretic
-  Polymorphism is set theoretic, constructively