Technical reports

The revised logic PPLAMBDA
A reference manual

Lawrence Paulson

March 1983, 28 pages

DOI: 10.48456/tr-36

Abstract

PPLAMBDA is the logic used in the Cambridge LCF proof assistant. It allows Natural Deduction proofs about computation, in Scott’s theory of partial orderings. The logic’s syntax, axioms, primitive inference rules, derived inference rules and standard lemmas are described as are the LCF functions for building and taking apart PPLAMBDA formulas.

PPLAMBDA’s rule of fixed-point induction admits a wide class of inductions, particularly where flat or finite types are involved. The user can express and prove these type properties in PPLAMBDA. The induction rule accepts a list of theorems, stating type properties to consider when deciding to admit an induction.

Full text

PDF (0.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-36,
  author =	 {Paulson, Lawrence},
  title = 	 {{The revised logic PPLAMBDA : A reference manual}},
  year = 	 1983,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-36.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-36},
  number = 	 {UCAM-CL-TR-36}
}