Technical reports

Automating recursive type definitions in higher order logic

Thomas F. Melham

September 1988, 64 pages

Abstract

The expressive power of higher order logic makes it possible to define a wide variety of types within the logic and to prove theorems that state the properties of these types concisely and abstractly. This paper contains a tutorial introduction to the logical basis for such type definitions. Examples are given of the formal definitions in logic of several simple types. A method is then described for systematically defining any instance of a certain class of commonly-used recursive types. The automation of this method in HOL, an interactive system for generating proofs in higher order logic, is also discussed.

Full text

PDF (5.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-146,
  author =	 {Melham, Thomas F.},
  title = 	 {{Automating recursive type definitions in higher order
         	   logic}},
  year = 	 1988,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-146.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-146},
  number = 	 {UCAM-CL-TR-146}
}