PPLambda(ID:1353/ppl002)

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

Structures:
Related languages
Cambridge LCF => PPLambda   Component of
References:
  • Paulson, LC "Lessons learned from LCF: a survey of natural deduction proofs" pp474-479 view details
          in The Computer Journal 28(5) 1985 view details
  • Paulson, L. "Logic and Computation: Interactive Proof with Cambridge LCF", Cambridge U Press, 1987. view details
          in The Computer Journal 28(5) 1985 view details