essentially the first-order predicate calculus superposed upon the simply-typed {polymorphic lAMbda-calculus}. PPLAMbda is the {object language} for LCF. ["Logic and Computation: Interactive Proof with CAMbridge LCF", L. Paulson, CAMbridge U Press, 1987]. (1995-05-01)