HOST pedigree

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.

Combining the paradigms Carnap (for one) uses higher order set theory. Liberal conservative extension added to HOL. ZF/HOL.

HOST rationale	HOST is a Mathematical Foundation System, Are Foundations Necessary?	HOST features