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.

@article{paperbot1211,
  title = {Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic},
  author = {Frank S. de Boer and Hans-Dieter A. Hiep},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {43},
  number = {4},
  year = {2021},
  doi = {10.1145/3477143}
}