Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. Pitts described the framework of hyperdoctrine models and topos models[3] which are consistent with constructive logic.

Presumably relational hyperdoctrine and topos models where then developed. Where can I read about them?

• [1] Types, abstraction and parametric polymorphism
• [2] Polymorphism is not set-theoretic
• [3] Polymorphism is set theoretic, constructively

Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. Pitts described the framework of hyperdoctrine models and topos models[3] which are consistent with constructive logic.

Presumably relational hyperdoctrine and topos models were then developed. Where can I read about them?

• [1] Types, abstraction and parametric polymorphism
• [2] Polymorphism is not set-theoretic
• [3] Polymorphism is set theoretic, constructively