Relating two models of hardware
The work
| Authors | Glynn Winskel |
|---|---|
| Editors | David H. Pitt; Axel Poigné; David E. Rydeheard |
| Type | incollection |
| Year | 1987 |
| Citekey | winskel1987relating |
Where it appeared
| Published in | Category Theory and Computer Science |
|---|---|
| Publisher | Springer Berlin Heidelberg |
| Series | Lecture Notes in Computer Science |
| Number in series | 283 |
| Pages | 98--113 |
Identifiers
| DOI | 10.1007/3-540-18508-9_22 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-540-18508-6 |
Access
| Landing page | https://doi.org/10.1007/3-540-18508-9_22 |
|---|---|
| Free full text | https://www.cl.cam.ac.uk/~gw104/Winskel1987_Chapter_RelatingTwoModelsOfHardware.pdf |
Related
| Distinct from | camilleri1986hardware |
|---|---|
| Distinct from | cardelli1982algebraic |
| Distinct from | clocksin1985logic |
| Distinct from | cohn1988correctness |
| Distinct from | cousot1977abstract |
| Distinct from | curzon1994formal |
| Distinct from | ferres2023electrical |
| Distinct from | ferres2025survey |
| Distinct from | fuegger2014faithful |
| Distinct from | fugger2016unfaithful |
| Distinct from | gordon1985why |
| Distinct from | leeser1988reasoning |
| Distinct from | melham1988using |
| Distinct from | melham1990formalizing |
| Distinct from | oulkaid2025modeles |
| Distinct from | paulson2018michael |
| Distinct from | seger1995formal |
| Distinct from | winskel1987models |
| Distinct from | winskel1988compositional |
| Distinct from | zhu2026equivfusion |
From crossref.
Abstract
The idea of this note is to show how Winskel's static-configuration model of circuits is related formally to Gordon's relational model. Once so related the simpler proofs in the Gordon model can, for instance, be used to justify results in terms of the Winskel model. More importantly, we can exhibit general conditions on circuits which ensure that assertions which hold of a circuit according to the simpler model are correct with respect to the more accurate model. The formal translation makes use of a simple adjunction between (partial order) categories associated with the two models, in a way reminiscent of abstract interpretation. Preliminary results suggest similar lines of approach may work for other kinds of abstraction such as temporal abstraction in reasoning about hardware, and, more generally, make possible a formal algebraic treatment of the relationship between different models of hardware.
A copy is held
pdf, 971.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 crossref |
|---|---|
| Added | 2026-09-15 23:13 UTC |
| Approved by | a person 2026-10-02 09:57 UTC |
Cite it as
@incollection{winskel1987relating,
title = {Relating two models of hardware},
author = {Glynn Winskel},
editor = {David H. Pitt and Axel Poigné and David E. Rydeheard},
year = {1987},
booktitle = {Category Theory and Computer Science},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
pages = {98--113},
isbn = {978-3-540-18508-6},
issn = {0302-9743},
doi = {10.1007/3-540-18508-9_22},
}
This record lives at https://refs.drheap.org/winskel1987relating/ and will keep doing so.