Using recursive types to reason about hardware in higher order logic
The work
| Authors | Thomas F. Melham |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1988 |
| Also known as | melham2021using |
| Citekey | melham1988using |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|
Identifiers
| DOI | 10.48456/tr-135 |
|---|---|
| OpenAlex | W1552543875 |
| report_number | UCAM-CL-TR-135 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-135.html |
|---|
Related
| Distinct from | baty2024formal |
|---|---|
| Distinct from | camilleri1986hardware |
| Distinct from | dhingra1987formal |
| Distinct from | dhingra1988formalising |
| Distinct from | gordon1985hol |
| Distinct from | melham1989automating |
| Distinct from | melham1990formalizing |
| Distinct from | ploix2025comprehensive |
| Distinct from | winskel1987relating |
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 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.
A copy is held
pdf, 305.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-16 10:33 UTC |
| Approved by | a person 2026-09-23 14:11 UTC |
Cite it as
@techreport{melham1988using,
title = {Using recursive types to reason about hardware in higher order logic},
author = {Thomas F. Melham},
year = {1988},
publisher = {University of Cambridge Computer Laboratory},
doi = {10.48456/tr-135},
}
This record lives at https://refs.drheap.org/melham1988using/ and will keep
doing so. It used to be called melham2021using, and those addresses still resolve to this one.