Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic
The work
| Authors | Frank S. de Boer; Hans-Dieter A. Hiep |
|---|---|
| Type | article |
| Year | 2021 |
| Citekey | boer2021completeness |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 43 |
| Issue | 4 |
| Pages | 17:1--17:35 |
Identifiers
| DOI | 10.1145/3477143 |
|---|---|
| OpenAlex | W3210461265 |
Access
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3477143 |
|---|---|
| Landing page | https://doi.org/10.1145/3477143 |
Abstract
We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.
A copy is held
pdf, 759.6 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-08-04 00:00 UTC |
| Approved by | a person 2026-08-26 09:45 UTC |
Filed under
Cite it as
@article{boer2021completeness,
title = {Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic},
author = {Frank S. de Boer and Hans-Dieter A. Hiep},
year = {2021},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {4},
pages = {17:1--17:35},
publisher = {Association for Computing Machinery},
doi = {10.1145/3477143},
}
This record lives at https://refs.drheap.org/boer2021completeness/ and will keep doing so.