pplambda

from The Free On-line Dictionary of Computing (8 July 2008)

PPLambda

   <language> 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)