Technical reports

Using recursive types to reason about hardware in higher order logic

Thomas F. Melham

May 1988, 30 pages

DOI: 10.48456/tr-135

Abstract

The expressive power of higher order logic makes it possible to define a wide variety of data types within the logic and to prove theorems that state the properties of these types concisely and abstractly. This paper describes how such defined data types can be used to support formal reasoning in higher order logic about the behaviour of hardware designs.

Full text

PDF (1.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-135,
  author =	 {Melham, Thomas F.},
  title = 	 {{Using recursive types to reason about hardware in higher
         	   order logic}},
  year = 	 1988,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-135.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-135},
  number = 	 {UCAM-CL-TR-135}
}