Features
Classical set theory formalised in a polymorphic higher order logic based on the typed lambda calculus.


Rationale
Set theory gives clean semantics with logical strength, polymorphic higher order logic enables all operators to be in the domain of discourse, building on the lambda calculus gives openended uniform support for variable binding constructs.


Pedigree
Cantor, Zermelo and Fraenkel were the main sources of the set theory, Frege, Russell and Church contributed the predicate calculus, the type theory, and its realisation throught the lambda calculus.
Robin Milner contributed the polymorphism, Mike Gordon first applied it to Church's logic.


Implementation
to adopt the LCF paradigm, with some further innovations, the most radical being the incorporation of a programming language in the logical kernel. 
