Why higher-order logic is a good formalism for specifying and verifying hardware
The work
| Authors | Mike Gordon |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1985 |
| Citekey | gordon1985why |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-77 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| report_number | UCAM-CL-TR-77 |
|---|---|
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-77.html |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | basin1991formally |
| Distinct from | camilleri1986hardware |
| Distinct from | camilleri1988simulation |
| Distinct from | clocksin1985logic |
| Distinct from | dhingra1988formalising |
| Distinct from | gammie2013synchronous |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985hol |
| Distinct from | gordon1987hol |
| Distinct from | guzmanmiranda2025fvm |
| Distinct from | herbert1988case |
| Distinct from | joyce1986proving |
| Distinct from | joyce1987hardware |
| Distinct from | paulson2018michael |
| Distinct from | winskel1987relating |
From bibtex.
Abstract
Higher-order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language and 2. a formalism for proving that designs meet their specifications. Examples are given which illustrate various specification and verification techniques. These include a CMOS inverter, a CMOS full adder, an n-bit ripple-carry adder, a sequential multiplier and an edge-triggered Dtype register.
A copy is held
pdf, 838.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 22:14 UTC |
| Approved by | a person 2026-09-16 09:23 UTC |
Cite it as
@techreport{gordon1985why,
title = {Why higher-order logic is a good formalism for specifying and verifying hardware},
author = {Mike Gordon},
year = {1985},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
}
This record lives at https://refs.drheap.org/gordon1985why/ and will keep doing so.