A general framework for sound and complete Floyd-Hoare logics

The work

TitleA general framework for sound and complete Floyd-Hoare logics
AuthorsRob Arthan; Ursula Martin; Erik A. Mathiesen; Paulo Oliva
Typearticle
Year2009
Citekeyarthan2009general

Where it appeared

Published inACM Transactions on Computational Logic
PublisherAssociation for Computing Machinery
Volume11
Issue1
Pages1--31

Identifiers

DOI10.1145/1614431.1614438
OpenAlexW2084929300

Access

Landing pagehttps://doi.org/10.1145/1614431.1614438
Free full texthttps://arxiv.org/pdf/0807.1016

Abstract

This article presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of preorders and monotone relations. We give several examples of how our theory generalizes usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (runtime analysis of while programs and stream circuits).

Copy held

KindPDF, 325.4 kB
Retrieved2026-08-05
Heldlocal, for personal reference
Where it came fromhttps://arxiv.org/pdf/0807.1016

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Standingendorsed
Approved2026-08-06

Cite it as

@article{arthan2009general,
  title = {A general framework for sound and complete Floyd-Hoare logics},
  author = {Rob Arthan and Ursula Martin and Erik A. Mathiesen and Paulo Oliva},
  year = {2009},
  journal = {ACM Transactions on Computational Logic},
  volume = {11},
  number = {1},
  pages = {1--31},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/1614431.1614438},
  url = {https://arxiv.org/pdf/0807.1016},
}

This record lives at https://refs.drheap.org/arthan2009general/ and will keep doing so.