Automating recursive type definitions in higher order logic

The work

AuthorsThomas Frederick Melham
Editors
Typetechreport
Year1988
Also known asmelham2021automating
Citekeymelham1988automating

Where it appeared

Published inCL Technical Reports
Number in seriesUCAM-CL-TR-146

Identifiers

DOI10.48456/tr-146
OpenAlexW6947790250
report_numberUCAM-CL-TR-146

Access

Landing pagehttps://doi.org/10.48456/tr-146

Related

Superseded bymelham1989automating

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

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.

A copy is held

pdf, 5.3 MB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-10-22 17:31 UTC
Approved bya person 2026-10-22 17:34 UTC

Filed under

melham what-one-proves-with

Cite it as

@techreport{melham1988automating,
  title        = {Automating recursive type definitions in higher order logic},
  author       = {Thomas Frederick Melham},
  year         = {1988},
  journal      = {CL Technical Reports},
  doi          = {10.48456/tr-146},
}

This record lives at https://refs.drheap.org/melham1988automating/ and will keep doing so. It used to be called melham2021automating, and those addresses still resolve to this one.