Higher Order Logic
 Bertrand Russell invents The Theory of Types [Russell08].
 Alonzo Church invents first the lambda calculus and then his Simple Theory of Types (STT), a radically simplfied but powerful type theory.
 Robin Milner invents a simple form of polymorphism for typed lambda cacluli in the course of implementing a proof tool for Scott's Logic for Computable Functions (LCF).
 Mike Gordon combines Church's STT with Milner polymorphism and conservative extension features in his LCF derived implementation of HOL.


Set Theory
 Cantor is the originator of informal modern set theory.
 Ernst Zermelo provided the first consistent axiomatisation in 1908
 Fraenkel adds the replacement axiom to increase the proof theoretic strength of Zermelo's system.
 Jean Raymond Abrial elaborates ZF set theory into the Z specification language which is used with freewheeling axiomatic extension and no apparent regard for conservative extension.

