Technical reports

A formulation of the simple theory of types (for Isabelle)

Lawrence C. Paulson

August 1989, 32 pages

DOI: 10.48456/tr-175

Abstract

Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed.

Isabelle proof procedures are described. The logic appears suitable for general mathematics as well as computational problems.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-175,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{A formulation of the simple theory of types (for Isabelle)}},
  year = 	 1989,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-175},
  number = 	 {UCAM-CL-TR-175}
}