Department of Computer Science and Technology

Technical reports

Automating recursive type definitions in higher order logic

Thomas F. Melham

September 1988, 64 pages

DOI: 10.48456/tr-146


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

  author =	 {Melham, Thomas F.},
  title = 	 {{Automating recursive type definitions in higher order
  year = 	 1988,
  month = 	 sep,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-146},
  number = 	 {UCAM-CL-TR-146}