The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Soundness of Hoare's logic: an automated proof using LCF
The work
| Authors | Stefan Sokołowski |
|---|---|
| Editors | |
| Type | article |
| Year | 1987 |
| Citekey | sokolowski1987soundness |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 9 |
| Issue | 1 |
| Pages | 100--121 |
Identifiers
| DOI | 10.1145/9758.11326 |
|---|---|
| OpenAlex | W1979753046 |
Access
| Landing page | https://doi.org/10.1145/9758.11326 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/9758.11326 |
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
This paper presents a natural deduction proof of Hoare's logic carried out by the Edinburgh LCF theorem prover. The emphasis is on the way Hoare's theory is presented to the LCF, which looks very much like an exposition of syntax and semantics to human readers; and on the programmable heuristics (tactics). We also discuss some problems and possible improvements to the LCF.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 06:41 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{sokolowski1987soundness,
title = {Soundness of Hoare's logic: an automated proof using LCF},
author = {Stefan Sokołowski},
year = {1987},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery},
volume = {9},
number = {1},
pages = {100--121},
doi = {10.1145/9758.11326},
}
This record lives at https://refs.drheap.org/sokolowski1987soundness/ and will keep doing so.