Using Nuprl for the verification and synthesis of hardware
The work
| Authors | Miriam E. Leeser |
|---|---|
| Editors | |
| Type | article |
| Year | 1992 |
| Citekey | leeser1992using |
Where it appeared
| Published in | Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences |
|---|---|
| Publisher | Royal Society |
| Volume | 339 |
| Issue | 1652 |
| Pages | 49--68 |
Identifiers
| DOI | 10.1098/rsta.1992.0025 |
|---|---|
| OpenAlex | W1560390462 |
Access
| Landing page | https://doi.org/10.1098/rsta.1992.0025 |
|---|
Related
| Reprinted as | leeser1992usingb |
|---|
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
Abstract The Nuprl proof development system, based on constructive type theory, has a sophisticated proof editor and user interface which facilitates the development of proofs and specifications. We present our experience using Nuprl for hardware verification and. synthesis. We have verified floating point hardware and are extending this work to reasoning about the IEEE floating point specification. In addition we are using Nuprl to reason about software for synthesizing hardware designs at several different levels. We present two efforts in this area. In the first, we prove a system that synthesizes CMOS circuits from boolean equations. The second system, PBS, minimizes large sets of boolean formulae by using the weak division algorithm.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 10:39 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{leeser1992using,
title = {Using Nuprl for the verification and synthesis of hardware},
author = {Miriam E. Leeser},
year = {1992},
journal = {Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences},
publisher = {Royal Society},
volume = {339},
number = {1652},
pages = {49--68},
doi = {10.1098/rsta.1992.0025},
}
This record lives at https://refs.drheap.org/leeser1992using/ and will keep doing so.