Technical reports
Automating recursive type definitions in higher order logic
Thomas F. Melham
September 1988, 64 pages
DOI: 10.48456/tr-146
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} }