essentially the first-ORder predicate calculus superposed upon the simply-typed {polymORphic lambda-calculus}. PPLambda is the {object language} fORLCF. ["Logic and Computation: Interactive Proof with Cambridge LCF", L. Paulson, Cambridge U Press, 1987]. (1995-05-01)