PPLambda

Essentially the first-order predicate calculus superposed upon the simply-typed polymorphic lambda-calculus. The object language for LCF.

"Logic and Computation: Interactive Proof with Cambridge LCF", L. Paulson, Cambridge University Press, 1987.