Source : Free On-Line Dictionary of Computing

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